Bundled non-unital subsemirings #
We define bundled non-unital subsemirings and some standard constructions:
CompleteLattice structure, subtype and inclusion ring homomorphisms, non-unital subsemiring
map, comap and range (srange) of a NonUnitalRingHom etc.
class
NonUnitalSubsemiringClass
(S : Type u_1)
(R : Type u)
[NonUnitalNonAssocSemiring R]
[SetLike S R]
extends
AddSubmonoidClass
:
NonUnitalSubsemiringClass S R states that S is a type of subsets s ⊆ R that
are both an additive submonoid and also a multiplicative subsemigroup.
- zero_mem : ∀ (s : S), 0 ∈ s
instance
NonUnitalSubsemiringClass.mulMemClass
(S : Type u_1)
(R : Type u)
[NonUnitalNonAssocSemiring R]
[SetLike S R]
[h : NonUnitalSubsemiringClass S R]
:
MulMemClass S R
Equations
- ⋯ = ⋯
instance
NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[SetLike S R]
[NonUnitalSubsemiringClass S R]
(s : S)
:
A non-unital subsemiring of a NonUnitalNonAssocSemiring inherits a
NonUnitalNonAssocSemiring structure
Equations
- NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring s = Function.Injective.nonUnitalNonAssocSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯
instance
NonUnitalSubsemiringClass.noZeroDivisors
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[SetLike S R]
[NonUnitalSubsemiringClass S R]
(s : S)
[NoZeroDivisors R]
:
Equations
- ⋯ = ⋯
def
NonUnitalSubsemiringClass.subtype
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[SetLike S R]
[NonUnitalSubsemiringClass S R]
(s : S)
:
↥s →ₙ+* R
The natural non-unital ring hom from a non-unital subsemiring of a non-unital semiring R to
R.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonUnitalSubsemiringClass.coeSubtype
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[SetLike S R]
[NonUnitalSubsemiringClass S R]
(s : S)
:
⇑(NonUnitalSubsemiringClass.subtype s) = Subtype.val
instance
NonUnitalSubsemiringClass.toNonUnitalSemiring
{S : Type v}
(s : S)
{R : Type u_1}
[NonUnitalSemiring R]
[SetLike S R]
[NonUnitalSubsemiringClass S R]
:
A non-unital subsemiring of a NonUnitalSemiring is a NonUnitalSemiring.
Equations
- NonUnitalSubsemiringClass.toNonUnitalSemiring s = Function.Injective.nonUnitalSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯
instance
NonUnitalSubsemiringClass.toNonUnitalCommSemiring
{S : Type v}
(s : S)
{R : Type u_1}
[NonUnitalCommSemiring R]
[SetLike S R]
[NonUnitalSubsemiringClass S R]
:
A non-unital subsemiring of a NonUnitalCommSemiring is a NonUnitalCommSemiring.
Equations
- NonUnitalSubsemiringClass.toNonUnitalCommSemiring s = Function.Injective.nonUnitalCommSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯
Note: currently, there are no ordered versions of non-unital rings.
structure
NonUnitalSubsemiring
(R : Type u)
[NonUnitalNonAssocSemiring R]
extends
AddSubmonoid
:
Type u
A non-unital subsemiring of a non-unital semiring R is a subset s that is both an additive
submonoid and a semigroup.
- carrier : Set R
- zero_mem' : 0 ∈ self.carrier
The product of two elements of a subsemigroup belongs to the subsemigroup.
Instances For
- NonUnitalSubsemiring.instBotNonUnitalSubsemiring
- NonUnitalSubsemiring.instCompleteLatticeNonUnitalSubsemiring
- NonUnitalSubsemiring.instInfNonUnitalSubsemiring
- NonUnitalSubsemiring.instInfSetNonUnitalSubsemiring
- NonUnitalSubsemiring.instInhabitedNonUnitalSubsemiring
- NonUnitalSubsemiring.instNonUnitalSubsemiringClassNonUnitalSubsemiringInstSetLikeNonUnitalSubsemiring
- NonUnitalSubsemiring.instSetLikeNonUnitalSubsemiring
- NonUnitalSubsemiring.instTopNonUnitalSubsemiring
@[reducible]
abbrev
NonUnitalSubsemiring.toSubsemigroup
{R : Type u}
[NonUnitalNonAssocSemiring R]
(self : NonUnitalSubsemiring R)
:
Reinterpret a NonUnitalSubsemiring as a Subsemigroup.
Equations
- NonUnitalSubsemiring.toSubsemigroup self = { carrier := self.carrier, mul_mem' := ⋯ }
instance
NonUnitalSubsemiring.instSetLikeNonUnitalSubsemiring
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
SetLike (NonUnitalSubsemiring R) R
Equations
- NonUnitalSubsemiring.instSetLikeNonUnitalSubsemiring = { coe := fun (s : NonUnitalSubsemiring R) => s.carrier, coe_injective' := ⋯ }
theorem
NonUnitalSubsemiring.mem_carrier
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : NonUnitalSubsemiring R}
{x : R}
:
theorem
NonUnitalSubsemiring.ext
{R : Type u}
[NonUnitalNonAssocSemiring R]
{S : NonUnitalSubsemiring R}
{T : NonUnitalSubsemiring R}
(h : ∀ (x : R), x ∈ S ↔ x ∈ T)
:
S = T
Two non-unital subsemirings are equal if they have the same elements.
def
NonUnitalSubsemiring.copy
{R : Type u}
[NonUnitalNonAssocSemiring R]
(S : NonUnitalSubsemiring R)
(s : Set R)
(hs : s = ↑S)
:
Copy of a non-unital subsemiring with a new carrier equal to the old one. Useful to fix
definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonUnitalSubsemiring.coe_copy
{R : Type u}
[NonUnitalNonAssocSemiring R]
(S : NonUnitalSubsemiring R)
(s : Set R)
(hs : s = ↑S)
:
↑(NonUnitalSubsemiring.copy S s hs) = s
theorem
NonUnitalSubsemiring.copy_eq
{R : Type u}
[NonUnitalNonAssocSemiring R]
(S : NonUnitalSubsemiring R)
(s : Set R)
(hs : s = ↑S)
:
NonUnitalSubsemiring.copy S s hs = S
theorem
NonUnitalSubsemiring.toSubsemigroup_injective
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
Function.Injective NonUnitalSubsemiring.toSubsemigroup
theorem
NonUnitalSubsemiring.toSubsemigroup_strictMono
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
StrictMono NonUnitalSubsemiring.toSubsemigroup
theorem
NonUnitalSubsemiring.toSubsemigroup_mono
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
Monotone NonUnitalSubsemiring.toSubsemigroup
theorem
NonUnitalSubsemiring.toAddSubmonoid_injective
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
Function.Injective NonUnitalSubsemiring.toAddSubmonoid
theorem
NonUnitalSubsemiring.toAddSubmonoid_strictMono
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
StrictMono NonUnitalSubsemiring.toAddSubmonoid
theorem
NonUnitalSubsemiring.toAddSubmonoid_mono
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
Monotone NonUnitalSubsemiring.toAddSubmonoid
def
NonUnitalSubsemiring.mk'
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : Set R)
(sg : Subsemigroup R)
(hg : ↑sg = s)
(sa : AddSubmonoid R)
(ha : ↑sa = s)
:
Construct a NonUnitalSubsemiring R from a set s, a subsemigroup sg, and an additive
submonoid sa such that x ∈ s ↔ x ∈ sg ↔ x ∈ sa.
Equations
- NonUnitalSubsemiring.mk' s sg hg sa ha = { toAddSubmonoid := { toAddSubsemigroup := { carrier := s, add_mem' := ⋯ }, zero_mem' := ⋯ }, mul_mem' := ⋯ }
@[simp]
theorem
NonUnitalSubsemiring.coe_mk'
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{sg : Subsemigroup R}
(hg : ↑sg = s)
{sa : AddSubmonoid R}
(ha : ↑sa = s)
:
↑(NonUnitalSubsemiring.mk' s sg hg sa ha) = s
@[simp]
theorem
NonUnitalSubsemiring.mem_mk'
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{sg : Subsemigroup R}
(hg : ↑sg = s)
{sa : AddSubmonoid R}
(ha : ↑sa = s)
{x : R}
:
x ∈ NonUnitalSubsemiring.mk' s sg hg sa ha ↔ x ∈ s
@[simp]
theorem
NonUnitalSubsemiring.mk'_toSubsemigroup
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{sg : Subsemigroup R}
(hg : ↑sg = s)
{sa : AddSubmonoid R}
(ha : ↑sa = s)
:
NonUnitalSubsemiring.toSubsemigroup (NonUnitalSubsemiring.mk' s sg hg sa ha) = sg
@[simp]
theorem
NonUnitalSubsemiring.mk'_toAddSubmonoid
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{sg : Subsemigroup R}
(hg : ↑sg = s)
{sa : AddSubmonoid R}
(ha : ↑sa = s)
:
(NonUnitalSubsemiring.mk' s sg hg sa ha).toAddSubmonoid = sa
@[simp]
theorem
NonUnitalSubsemiring.coe_zero
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
:
↑0 = 0
@[simp]
theorem
NonUnitalSubsemiring.coe_add
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
(x : ↥s)
(y : ↥s)
:
@[simp]
theorem
NonUnitalSubsemiring.coe_mul
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
(x : ↥s)
(y : ↥s)
:
Note: currently, there are no ordered versions of non-unital rings.
@[simp]
theorem
NonUnitalSubsemiring.mem_toSubsemigroup
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : NonUnitalSubsemiring R}
{x : R}
:
x ∈ NonUnitalSubsemiring.toSubsemigroup s ↔ x ∈ s
@[simp]
theorem
NonUnitalSubsemiring.coe_toSubsemigroup
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
:
↑(NonUnitalSubsemiring.toSubsemigroup s) = ↑s
@[simp]
theorem
NonUnitalSubsemiring.mem_toAddSubmonoid
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : NonUnitalSubsemiring R}
{x : R}
:
@[simp]
theorem
NonUnitalSubsemiring.coe_toAddSubmonoid
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
:
↑s.toAddSubmonoid = ↑s
instance
NonUnitalSubsemiring.instTopNonUnitalSubsemiring
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
The non-unital subsemiring R of the non-unital semiring R.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
@[simp]
theorem
NonUnitalSubsemiring.topEquiv_symm_apply_coe
{R : Type u}
[NonUnitalNonAssocSemiring R]
(x : R)
:
↑((RingEquiv.symm NonUnitalSubsemiring.topEquiv) x) = x
@[simp]
theorem
NonUnitalSubsemiring.topEquiv_apply
{R : Type u}
[NonUnitalNonAssocSemiring R]
(x : ↥⊤)
:
NonUnitalSubsemiring.topEquiv x = ↑x
The ring equiv between the top element of NonUnitalSubsemiring R and R.
Equations
- NonUnitalSubsemiring.topEquiv = let __src := Subsemigroup.topEquiv; let __src_1 := AddSubmonoid.topEquiv; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }
def
NonUnitalSubsemiring.comap
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(s : NonUnitalSubsemiring S)
:
The preimage of a non-unital subsemiring along a non-unital ring homomorphism is a non-unital subsemiring.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonUnitalSubsemiring.coe_comap
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(s : NonUnitalSubsemiring S)
(f : F)
:
↑(NonUnitalSubsemiring.comap f s) = ⇑f ⁻¹' ↑s
@[simp]
theorem
NonUnitalSubsemiring.mem_comap
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{s : NonUnitalSubsemiring S}
{f : F}
{x : R}
:
x ∈ NonUnitalSubsemiring.comap f s ↔ f x ∈ s
theorem
NonUnitalSubsemiring.comap_comap
{R : Type u}
{S : Type v}
{T : Type w}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
[NonUnitalNonAssocSemiring T]
{F : Type u_1}
{G : Type u_2}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
[FunLike G S T]
[NonUnitalRingHomClass G S T]
(s : NonUnitalSubsemiring T)
(g : G)
(f : F)
:
def
NonUnitalSubsemiring.map
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(s : NonUnitalSubsemiring R)
:
The image of a non-unital subsemiring along a ring homomorphism is a non-unital subsemiring.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonUnitalSubsemiring.coe_map
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(s : NonUnitalSubsemiring R)
:
↑(NonUnitalSubsemiring.map f s) = ⇑f '' ↑s
@[simp]
theorem
NonUnitalSubsemiring.mem_map
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{f : F}
{s : NonUnitalSubsemiring R}
{y : S}
:
y ∈ NonUnitalSubsemiring.map f s ↔ ∃ x ∈ s, f x = y
@[simp]
theorem
NonUnitalSubsemiring.map_id
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
:
theorem
NonUnitalSubsemiring.map_map
{R : Type u}
{S : Type v}
{T : Type w}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
[NonUnitalNonAssocSemiring T]
{F : Type u_1}
{G : Type u_2}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
[FunLike G S T]
[NonUnitalRingHomClass G S T]
(s : NonUnitalSubsemiring R)
(g : G)
(f : F)
:
NonUnitalSubsemiring.map (↑g) (NonUnitalSubsemiring.map (↑f) s) = NonUnitalSubsemiring.map (NonUnitalRingHom.comp ↑g ↑f) s
theorem
NonUnitalSubsemiring.map_le_iff_le_comap
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{f : F}
{s : NonUnitalSubsemiring R}
{t : NonUnitalSubsemiring S}
:
NonUnitalSubsemiring.map f s ≤ t ↔ s ≤ NonUnitalSubsemiring.comap f t
theorem
NonUnitalSubsemiring.gc_map_comap
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
noncomputable def
NonUnitalSubsemiring.equivMapOfInjective
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(s : NonUnitalSubsemiring R)
(f : F)
(hf : Function.Injective ⇑f)
:
↥s ≃+* ↥(NonUnitalSubsemiring.map f s)
A non-unital subsemiring is isomorphic to its image under an injective function
Equations
- NonUnitalSubsemiring.equivMapOfInjective s f hf = let __src := Equiv.Set.image (⇑f) (↑s) hf; { toEquiv := __src, map_mul' := ⋯, map_add' := ⋯ }
@[simp]
theorem
NonUnitalSubsemiring.coe_equivMapOfInjective_apply
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(s : NonUnitalSubsemiring R)
(f : F)
(hf : Function.Injective ⇑f)
(x : ↥s)
:
↑((NonUnitalSubsemiring.equivMapOfInjective s f hf) x) = f ↑x
def
NonUnitalRingHom.srange
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
The range of a non-unital ring homomorphism is a non-unital subsemiring. See note [range copy pattern].
Equations
@[simp]
theorem
NonUnitalRingHom.coe_srange
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
↑(NonUnitalRingHom.srange f) = Set.range ⇑f
@[simp]
theorem
NonUnitalRingHom.mem_srange
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{f : F}
{y : S}
:
y ∈ NonUnitalRingHom.srange f ↔ ∃ (x : R), f x = y
theorem
NonUnitalRingHom.srange_eq_map
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
theorem
NonUnitalRingHom.mem_srange_self
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(x : R)
:
f x ∈ NonUnitalRingHom.srange f
theorem
NonUnitalRingHom.map_srange
{R : Type u}
{S : Type v}
{T : Type w}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
[NonUnitalNonAssocSemiring T]
(g : S →ₙ+* T)
(f : R →ₙ+* S)
:
instance
NonUnitalRingHom.finite_srange
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
[Finite R]
(f : F)
:
The range of a morphism of non-unital semirings is finite if the domain is a finite.
Equations
- ⋯ = ⋯
instance
NonUnitalSubsemiring.instBotNonUnitalSubsemiring
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
Equations
- NonUnitalSubsemiring.instBotNonUnitalSubsemiring = { bot := { toAddSubmonoid := { toAddSubsemigroup := { carrier := {0}, add_mem' := ⋯ }, zero_mem' := ⋯ }, mul_mem' := ⋯ } }
instance
NonUnitalSubsemiring.instInhabitedNonUnitalSubsemiring
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
instance
NonUnitalSubsemiring.instInfNonUnitalSubsemiring
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
The inf of two non-unital subsemirings is their intersection.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonUnitalSubsemiring.coe_inf
{R : Type u}
[NonUnitalNonAssocSemiring R]
(p : NonUnitalSubsemiring R)
(p' : NonUnitalSubsemiring R)
:
@[simp]
theorem
NonUnitalSubsemiring.mem_inf
{R : Type u}
[NonUnitalNonAssocSemiring R]
{p : NonUnitalSubsemiring R}
{p' : NonUnitalSubsemiring R}
{x : R}
:
instance
NonUnitalSubsemiring.instInfSetNonUnitalSubsemiring
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonUnitalSubsemiring.coe_sInf
{R : Type u}
[NonUnitalNonAssocSemiring R]
(S : Set (NonUnitalSubsemiring R))
:
theorem
NonUnitalSubsemiring.mem_sInf
{R : Type u}
[NonUnitalNonAssocSemiring R]
{S : Set (NonUnitalSubsemiring R)}
{x : R}
:
@[simp]
theorem
NonUnitalSubsemiring.sInf_toSubsemigroup
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : Set (NonUnitalSubsemiring R))
:
@[simp]
theorem
NonUnitalSubsemiring.sInf_toAddSubmonoid
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : Set (NonUnitalSubsemiring R))
:
instance
NonUnitalSubsemiring.instCompleteLatticeNonUnitalSubsemiring
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
Non-unital subsemirings of a non-unital semiring form a complete lattice.
Equations
- NonUnitalSubsemiring.instCompleteLatticeNonUnitalSubsemiring = let __src := completeLatticeOfInf (NonUnitalSubsemiring R) ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
NonUnitalSubsemiring.eq_top_iff'
{R : Type u}
[NonUnitalNonAssocSemiring R]
(A : NonUnitalSubsemiring R)
:
The center of a semiring R is the set of elements that commute and associate with everything
in R
Equations
- NonUnitalSubsemiring.center R = let __src := Subsemigroup.center R; { toAddSubmonoid := { toAddSubsemigroup := { carrier := __src.carrier, add_mem' := ⋯ }, zero_mem' := ⋯ }, mul_mem' := ⋯ }
@[simp]
instance
NonUnitalSubsemiring.center.instNonUnitalCommSemiring
(R : Type u)
[NonUnitalNonAssocSemiring R]
:
The center is commutative and associative.
Equations
- One or more equations did not get rendered due to their size.
theorem
Set.mem_center_iff_addMonoidHom
(R : Type u)
[NonUnitalNonAssocSemiring R]
(a : R)
:
a ∈ Set.center R ↔ AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧ AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulLeft a) = AddMonoidHom.comp AddMonoidHom.mul (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.comp AddMonoidHom.mul (AddMonoidHom.mulRight a) = AddMonoidHom.compl₂ AddMonoidHom.mul (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulRight a) = AddMonoidHom.compl₂ AddMonoidHom.mul (AddMonoidHom.mulRight a)
A point-free means of proving membership in the center, for a non-associative ring.
This can be helpful when working with types that have ext lemmas for R →+ R.
instance
NonUnitalSubsemiring.decidableMemCenter
{R : Type u_1}
[NonUnitalSemiring R]
[DecidableEq R]
[Fintype R]
:
DecidablePred fun (x : R) => x ∈ NonUnitalSubsemiring.center R
Equations
- NonUnitalSubsemiring.decidableMemCenter x = decidable_of_iff' (∀ (g : R), g * x = x * g) ⋯
@[simp]
The centralizer of a set as non-unital subsemiring.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonUnitalSubsemiring.centralizer_toSubsemigroup
{R : Type u_1}
[NonUnitalSemiring R]
(s : Set R)
:
theorem
NonUnitalSubsemiring.mem_centralizer_iff
{R : Type u_1}
[NonUnitalSemiring R]
{s : Set R}
{z : R}
:
theorem
NonUnitalSubsemiring.center_le_centralizer
{R : Type u_1}
[NonUnitalSemiring R]
(s : Set R)
:
theorem
NonUnitalSubsemiring.centralizer_le
{R : Type u_1}
[NonUnitalSemiring R]
(s : Set R)
(t : Set R)
(h : s ⊆ t)
:
@[simp]
theorem
NonUnitalSubsemiring.centralizer_eq_top_iff_subset
{R : Type u_1}
[NonUnitalSemiring R]
{s : Set R}
:
@[simp]
The NonUnitalSubsemiring generated by a set.
Equations
- NonUnitalSubsemiring.closure s = sInf {S : NonUnitalSubsemiring R | s ⊆ ↑S}
theorem
NonUnitalSubsemiring.mem_closure
{R : Type u}
[NonUnitalNonAssocSemiring R]
{x : R}
{s : Set R}
:
x ∈ NonUnitalSubsemiring.closure s ↔ ∀ (S : NonUnitalSubsemiring R), s ⊆ ↑S → x ∈ S
@[simp]
theorem
NonUnitalSubsemiring.subset_closure
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
:
s ⊆ ↑(NonUnitalSubsemiring.closure s)
The non-unital subsemiring generated by a set includes the set.
theorem
NonUnitalSubsemiring.not_mem_of_not_mem_closure
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{P : R}
(hP : P ∉ NonUnitalSubsemiring.closure s)
:
P ∉ s
@[simp]
theorem
NonUnitalSubsemiring.closure_le
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{t : NonUnitalSubsemiring R}
:
NonUnitalSubsemiring.closure s ≤ t ↔ s ⊆ ↑t
A non-unital subsemiring S includes closure s if and only if it includes s.
theorem
NonUnitalSubsemiring.closure_mono
{R : Type u}
[NonUnitalNonAssocSemiring R]
⦃s : Set R⦄
⦃t : Set R⦄
(h : s ⊆ t)
:
Subsemiring closure of a set is monotone in its argument: if s ⊆ t,
then closure s ≤ closure t.
theorem
NonUnitalSubsemiring.closure_eq_of_le
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{t : NonUnitalSubsemiring R}
(h₁ : s ⊆ ↑t)
(h₂ : t ≤ NonUnitalSubsemiring.closure s)
:
theorem
NonUnitalSubsemiring.mem_map_equiv
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{f : R ≃+* S}
{K : NonUnitalSubsemiring R}
{x : S}
:
x ∈ NonUnitalSubsemiring.map (↑f) K ↔ (RingEquiv.symm f) x ∈ K
theorem
NonUnitalSubsemiring.map_equiv_eq_comap_symm
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(f : R ≃+* S)
(K : NonUnitalSubsemiring R)
:
theorem
NonUnitalSubsemiring.comap_equiv_eq_map_symm
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(f : R ≃+* S)
(K : NonUnitalSubsemiring S)
:
def
Subsemigroup.nonUnitalSubsemiringClosure
{R : Type u}
[NonUnitalNonAssocSemiring R]
(M : Subsemigroup R)
:
The additive closure of a non-unital subsemigroup is a non-unital subsemiring.
Equations
- Subsemigroup.nonUnitalSubsemiringClosure M = let __src := AddSubmonoid.closure ↑M; { toAddSubmonoid := __src, mul_mem' := ⋯ }
theorem
Subsemigroup.nonUnitalSubsemiringClosure_coe
{R : Type u}
[NonUnitalNonAssocSemiring R]
(M : Subsemigroup R)
:
theorem
Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid
{R : Type u}
[NonUnitalNonAssocSemiring R]
(M : Subsemigroup R)
:
(Subsemigroup.nonUnitalSubsemiringClosure M).toAddSubmonoid = AddSubmonoid.closure ↑M
theorem
Subsemigroup.nonUnitalSubsemiringClosure_eq_closure
{R : Type u}
[NonUnitalNonAssocSemiring R]
(M : Subsemigroup R)
:
The NonUnitalSubsemiring generated by a multiplicative subsemigroup coincides with the
NonUnitalSubsemiring.closure of the subsemigroup itself .
@[simp]
theorem
NonUnitalSubsemiring.closure_subsemigroup_closure
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : Set R)
:
theorem
NonUnitalSubsemiring.coe_closure_eq
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : Set R)
:
The elements of the non-unital subsemiring closure of M are exactly the elements of the
additive closure of a multiplicative subsemigroup M.
theorem
NonUnitalSubsemiring.mem_closure_iff
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{x : R}
:
@[simp]
theorem
NonUnitalSubsemiring.closure_addSubmonoid_closure
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
:
theorem
NonUnitalSubsemiring.closure_induction
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{p : R → Prop}
{x : R}
(h : x ∈ NonUnitalSubsemiring.closure s)
(mem : ∀ x ∈ s, p x)
(zero : p 0)
(add : ∀ (x y : R), p x → p y → p (x + y))
(mul : ∀ (x y : R), p x → p y → p (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 and multiplication, then p holds for all elements
of the closure of s.
theorem
NonUnitalSubsemiring.closure_induction₂
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : Set R}
{p : R → R → Prop}
{x : R}
{y : R}
(hx : x ∈ NonUnitalSubsemiring.closure s)
(hy : y ∈ NonUnitalSubsemiring.closure s)
(Hs : ∀ x ∈ s, ∀ y ∈ s, p x y)
(H0_left : ∀ (x : R), p 0 x)
(H0_right : ∀ (x : R), p x 0)
(Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (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₁ y → p x₂ y → p (x₁ * x₂) y)
(Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂))
:
p x y
An induction principle for closure membership for predicates with two arguments.
def
NonUnitalSubsemiring.gi
(R : Type u)
[NonUnitalNonAssocSemiring R]
:
GaloisInsertion NonUnitalSubsemiring.closure SetLike.coe
closure forms a Galois insertion with the coercion to set.
Equations
- NonUnitalSubsemiring.gi R = { choice := fun (s : Set R) (x : ↑(NonUnitalSubsemiring.closure s) ≤ s) => NonUnitalSubsemiring.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
theorem
NonUnitalSubsemiring.closure_eq
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
:
Closure of a non-unital subsemiring S equals S.
@[simp]
@[simp]
theorem
NonUnitalSubsemiring.closure_univ
{R : Type u}
[NonUnitalNonAssocSemiring R]
:
NonUnitalSubsemiring.closure Set.univ = ⊤
theorem
NonUnitalSubsemiring.closure_union
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : Set R)
(t : Set R)
:
theorem
NonUnitalSubsemiring.closure_iUnion
{R : Type u}
[NonUnitalNonAssocSemiring R]
{ι : Sort u_2}
(s : ι → Set R)
:
NonUnitalSubsemiring.closure (⋃ (i : ι), s i) = ⨆ (i : ι), NonUnitalSubsemiring.closure (s i)
theorem
NonUnitalSubsemiring.closure_sUnion
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : Set (Set R))
:
NonUnitalSubsemiring.closure (⋃₀ s) = ⨆ t ∈ s, NonUnitalSubsemiring.closure t
theorem
NonUnitalSubsemiring.map_sup
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(s : NonUnitalSubsemiring R)
(t : NonUnitalSubsemiring R)
(f : F)
:
NonUnitalSubsemiring.map f (s ⊔ t) = NonUnitalSubsemiring.map f s ⊔ NonUnitalSubsemiring.map f t
theorem
NonUnitalSubsemiring.map_iSup
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{ι : Sort u_2}
(f : F)
(s : ι → NonUnitalSubsemiring R)
:
NonUnitalSubsemiring.map f (iSup s) = ⨆ (i : ι), NonUnitalSubsemiring.map f (s i)
theorem
NonUnitalSubsemiring.comap_inf
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(s : NonUnitalSubsemiring S)
(t : NonUnitalSubsemiring S)
(f : F)
:
NonUnitalSubsemiring.comap f (s ⊓ t) = NonUnitalSubsemiring.comap f s ⊓ NonUnitalSubsemiring.comap f t
theorem
NonUnitalSubsemiring.comap_iInf
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{ι : Sort u_2}
(f : F)
(s : ι → NonUnitalSubsemiring S)
:
NonUnitalSubsemiring.comap f (iInf s) = ⨅ (i : ι), NonUnitalSubsemiring.comap f (s i)
@[simp]
theorem
NonUnitalSubsemiring.map_bot
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
@[simp]
theorem
NonUnitalSubsemiring.comap_top
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
def
NonUnitalSubsemiring.prod
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(s : NonUnitalSubsemiring R)
(t : NonUnitalSubsemiring S)
:
NonUnitalSubsemiring (R × S)
Given NonUnitalSubsemirings s, t of semirings R, S respectively, s.prod t is
s × t as a non-unital subsemiring of R × S.
Equations
- One or more equations did not get rendered due to their size.
theorem
NonUnitalSubsemiring.coe_prod
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(s : NonUnitalSubsemiring R)
(t : NonUnitalSubsemiring S)
:
↑(NonUnitalSubsemiring.prod s t) = ↑s ×ˢ ↑t
theorem
NonUnitalSubsemiring.mem_prod
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{s : NonUnitalSubsemiring R}
{t : NonUnitalSubsemiring S}
{p : R × S}
:
theorem
NonUnitalSubsemiring.prod_mono
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
⦃s₁ : NonUnitalSubsemiring R⦄
⦃s₂ : NonUnitalSubsemiring R⦄
(hs : s₁ ≤ s₂)
⦃t₁ : NonUnitalSubsemiring S⦄
⦃t₂ : NonUnitalSubsemiring S⦄
(ht : t₁ ≤ t₂)
:
NonUnitalSubsemiring.prod s₁ t₁ ≤ NonUnitalSubsemiring.prod s₂ t₂
theorem
NonUnitalSubsemiring.prod_mono_right
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(s : NonUnitalSubsemiring R)
:
Monotone fun (t : NonUnitalSubsemiring S) => NonUnitalSubsemiring.prod s t
theorem
NonUnitalSubsemiring.prod_mono_left
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(t : NonUnitalSubsemiring S)
:
Monotone fun (s : NonUnitalSubsemiring R) => NonUnitalSubsemiring.prod s t
theorem
NonUnitalSubsemiring.prod_top
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(s : NonUnitalSubsemiring R)
:
theorem
NonUnitalSubsemiring.top_prod
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(s : NonUnitalSubsemiring S)
:
@[simp]
theorem
NonUnitalSubsemiring.top_prod_top
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
:
def
NonUnitalSubsemiring.prodEquiv
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(s : NonUnitalSubsemiring R)
(t : NonUnitalSubsemiring S)
:
↥(NonUnitalSubsemiring.prod s t) ≃+* ↥s × ↥t
Product of non-unital subsemirings is isomorphic to their product as semigroups.
Equations
- NonUnitalSubsemiring.prodEquiv s t = let __src := Equiv.Set.prod ↑s ↑t; { toEquiv := __src, map_mul' := ⋯, map_add' := ⋯ }
theorem
NonUnitalSubsemiring.mem_iSup_of_directed
{R : Type u}
[NonUnitalNonAssocSemiring R]
{ι : Sort u_2}
[hι : Nonempty ι]
{S : ι → NonUnitalSubsemiring R}
(hS : Directed (fun (x x_1 : NonUnitalSubsemiring R) => x ≤ x_1) S)
{x : R}
:
theorem
NonUnitalSubsemiring.coe_iSup_of_directed
{R : Type u}
[NonUnitalNonAssocSemiring R]
{ι : Sort u_2}
[hι : Nonempty ι]
{S : ι → NonUnitalSubsemiring R}
(hS : Directed (fun (x x_1 : NonUnitalSubsemiring R) => x ≤ x_1) S)
:
↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)
theorem
NonUnitalSubsemiring.mem_sSup_of_directedOn
{R : Type u}
[NonUnitalNonAssocSemiring R]
{S : Set (NonUnitalSubsemiring R)}
(Sne : Set.Nonempty S)
(hS : DirectedOn (fun (x x_1 : NonUnitalSubsemiring R) => x ≤ x_1) S)
{x : R}
:
theorem
NonUnitalSubsemiring.coe_sSup_of_directedOn
{R : Type u}
[NonUnitalNonAssocSemiring R]
{S : Set (NonUnitalSubsemiring R)}
(Sne : Set.Nonempty S)
(hS : DirectedOn (fun (x x_1 : NonUnitalSubsemiring R) => x ≤ x_1) S)
:
def
NonUnitalRingHom.codRestrict
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{S' : Type u_2}
[SetLike S' S]
[NonUnitalSubsemiringClass S' S]
(f : F)
(s : S')
(h : ∀ (x : R), f x ∈ s)
:
R →ₙ+* ↥s
Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.
Equations
- NonUnitalRingHom.codRestrict f s h = { toMulHom := { toFun := fun (n : R) => { val := f n, property := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
def
NonUnitalRingHom.srangeRestrict
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
R →ₙ+* ↥(NonUnitalRingHom.srange f)
Restriction of a non-unital ring homomorphism to its range interpreted as a non-unital subsemiring.
This is the bundled version of Set.rangeFactorization.
Equations
@[simp]
theorem
NonUnitalRingHom.coe_srangeRestrict
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(x : R)
:
↑((NonUnitalRingHom.srangeRestrict f) x) = f x
theorem
NonUnitalRingHom.srangeRestrict_surjective
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
:
theorem
NonUnitalRingHom.srange_top_iff_surjective
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{f : F}
:
@[simp]
theorem
NonUnitalRingHom.srange_top_of_surjective
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(hf : Function.Surjective ⇑f)
:
The range of a surjective non-unital ring homomorphism is the whole of the codomain.
def
NonUnitalRingHom.eqSlocus
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(g : F)
:
The non-unital subsemiring of elements x : R such that f x = g x
Equations
- One or more equations did not get rendered due to their size.
theorem
NonUnitalRingHom.eqOn_sclosure
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{f : F}
{g : F}
{s : Set R}
(h : Set.EqOn (⇑f) (⇑g) s)
:
Set.EqOn ⇑f ⇑g ↑(NonUnitalSubsemiring.closure s)
If two non-unital ring homomorphisms are equal on a set, then they are equal on its non-unital subsemiring closure.
theorem
NonUnitalRingHom.eq_of_eqOn_stop
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
{F : Type u_1}
[FunLike F R S]
{f : F}
{g : F}
(h : Set.EqOn ⇑f ⇑g ↑⊤)
:
f = g
theorem
NonUnitalRingHom.eq_of_eqOn_sdense
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{s : Set R}
(hs : NonUnitalSubsemiring.closure s = ⊤)
{f : F}
{g : F}
(h : Set.EqOn (⇑f) (⇑g) s)
:
f = g
theorem
NonUnitalRingHom.sclosure_preimage_le
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(s : Set S)
:
theorem
NonUnitalRingHom.map_sclosure
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
(f : F)
(s : Set R)
:
The image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set.
def
NonUnitalSubsemiring.inclusion
{R : Type u}
[NonUnitalNonAssocSemiring R]
{S : NonUnitalSubsemiring R}
{T : NonUnitalSubsemiring R}
(h : S ≤ T)
:
↥S →ₙ+* ↥T
The non-unital ring homomorphism associated to an inclusion of non-unital subsemirings.
@[simp]
theorem
NonUnitalSubsemiring.srange_subtype
{R : Type u}
[NonUnitalNonAssocSemiring R]
(s : NonUnitalSubsemiring R)
:
@[simp]
theorem
NonUnitalSubsemiring.range_fst
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
:
@[simp]
theorem
NonUnitalSubsemiring.range_snd
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
:
def
RingEquiv.nonUnitalSubsemiringCongr
{R : Type u}
[NonUnitalNonAssocSemiring R]
{s : NonUnitalSubsemiring R}
{t : NonUnitalSubsemiring R}
(h : s = t)
:
↥s ≃+* ↥t
Makes the identity isomorphism from a proof two non-unital subsemirings of a multiplicative monoid are equal.
Equations
- RingEquiv.nonUnitalSubsemiringCongr h = let __src := Equiv.setCongr ⋯; { toEquiv := __src, map_mul' := ⋯, map_add' := ⋯ }
def
RingEquiv.sofLeftInverse'
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{g : S → R}
{f : F}
(h : Function.LeftInverse g ⇑f)
:
R ≃+* ↥(NonUnitalRingHom.srange f)
Restrict a non-unital ring homomorphism with a left inverse to a ring isomorphism to its
NonUnitalRingHom.srange.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
RingEquiv.sofLeftInverse'_apply
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{g : S → R}
{f : F}
(h : Function.LeftInverse g ⇑f)
(x : R)
:
↑((RingEquiv.sofLeftInverse' h) x) = f x
@[simp]
theorem
RingEquiv.sofLeftInverse'_symm_apply
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
{F : Type u_1}
[FunLike F R S]
[NonUnitalRingHomClass F R S]
{g : S → R}
{f : F}
(h : Function.LeftInverse g ⇑f)
(x : ↥(NonUnitalRingHom.srange f))
:
(RingEquiv.symm (RingEquiv.sofLeftInverse' h)) x = g ↑x
@[simp]
theorem
RingEquiv.nonUnitalSubsemiringMap_apply_coe
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(e : R ≃+* S)
(s : NonUnitalSubsemiring R)
(x : ↑↑s.toAddSubmonoid)
:
↑((RingEquiv.nonUnitalSubsemiringMap e s) x) = e ↑x
@[simp]
theorem
RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(e : R ≃+* S)
(s : NonUnitalSubsemiring R)
(y : ↑(⇑↑(RingEquiv.toAddEquiv e) '' ↑s.toAddSubmonoid))
:
↑((RingEquiv.symm (RingEquiv.nonUnitalSubsemiringMap e s)) y) = (AddEquiv.symm ↑e) ↑y
def
RingEquiv.nonUnitalSubsemiringMap
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
(e : R ≃+* S)
(s : NonUnitalSubsemiring R)
:
↥s ≃+* ↥(NonUnitalSubsemiring.map (RingEquiv.toNonUnitalRingHom e) s)
Given an equivalence e : R ≃+* S of non-unital semirings and a non-unital subsemiring
s of R, non_unital_subsemiring_map e s is the induced equivalence between s and
s.map e
Equations
- One or more equations did not get rendered due to their size.