Bundled subsemirings
We define bundled subsemirings and some standard constructions: complete_lattice structure,
subtype and inclusion ring homomorphisms, subsemiring map, comap and range (srange) of
a ring_hom etc.
Reinterpret a subsemiring as an add_submonoid.
Reinterpret a subsemiring as a submonoid.
- carrier : set R
- one_mem' : 1 ∈ c.carrier
- mul_mem' : ∀ {a b : R}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
- zero_mem' : 0 ∈ c.carrier
- add_mem' : ∀ {a b : R}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
A subsemiring of a semiring R is a subset s that is both a multiplicative and an additive
submonoid.
@[instance]
Equations
- subsemiring.has_coe = {coe := subsemiring.carrier _inst_1}
@[instance]
Equations
- subsemiring.has_coe_to_sort = {S := Type u, coe := λ (S : subsemiring R), ↥(S.carrier)}
@[instance]
Equations
- subsemiring.has_mem = {mem := λ (m : R) (S : subsemiring R), m ∈ ↑S}
def
subsemiring.mk'
{R : Type u}
[semiring R]
(s : set R)
(sm : submonoid R)
(hm : ↑sm = s)
(sa : add_submonoid R) :
↑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.
@[simp]
theorem
subsemiring.coe_mk'
{R : Type u}
[semiring R]
{s : set R}
{sm : submonoid R}
(hm : ↑sm = s)
{sa : add_submonoid R}
(ha : ↑sa = s) :
↑(subsemiring.mk' s sm hm sa ha) = s
@[simp]
theorem
subsemiring.mem_mk'
{R : Type u}
[semiring R]
{s : set R}
{sm : submonoid R}
(hm : ↑sm = s)
{sa : add_submonoid R}
(ha : ↑sa = s)
{x : R} :
x ∈ subsemiring.mk' s sm hm sa ha ↔ x ∈ s
@[simp]
theorem
subsemiring.mk'_to_submonoid
{R : Type u}
[semiring R]
{s : set R}
{sm : submonoid R}
(hm : ↑sm = s)
{sa : add_submonoid R}
(ha : ↑sa = s) :
(subsemiring.mk' s sm hm sa ha).to_submonoid = sm
@[simp]
theorem
subsemiring.mk'_to_add_submonoid
{R : Type u}
[semiring R]
{s : set R}
{sm : submonoid R}
(hm : ↑sm = s)
{sa : add_submonoid R}
(ha : ↑sa = s) :
(subsemiring.mk' s sm hm sa ha).to_add_submonoid = sa
Two subsemirings are equal if the underlying subsets are equal.
Two subsemirings are equal if and only if the underlying subsets are equal.
@[ext]
Two subsemirings are equal if they have the same elements.
A subsemiring contains the semiring's 1.
A subsemiring contains the semiring's 0.
A subsemiring is closed under multiplication.
A subsemiring is closed under addition.
Product of a list of elements in a subsemiring is in the subsemiring.
Sum of a list of elements in a subsemiring is in the subsemiring.
theorem
subsemiring.multiset_prod_mem
{R : Type u_1}
[comm_semiring R]
(s : subsemiring R)
(m : multiset R) :
Product of a multiset of elements in a subsemiring of a comm_semiring
is in the subsemiring.
theorem
subsemiring.multiset_sum_mem
{R : Type u_1}
[semiring R]
(s : subsemiring R)
(m : multiset R) :
Sum of a multiset of elements in a subsemiring of a semiring is
in the add_subsemiring.
theorem
subsemiring.prod_mem
{R : Type u_1}
[comm_semiring R]
(s : subsemiring R)
{ι : Type u_2}
{t : finset ι}
{f : ι → R} :
Product of elements of a subsemiring of a comm_semiring indexed by a finset is in the
subsemiring.
theorem
subsemiring.sum_mem
{R : Type u_1}
[semiring R]
(s : subsemiring R)
{ι : Type u_2}
{t : finset ι}
{f : ι → R} :
Sum of elements in an subsemiring of an semiring indexed by a finset
is in the add_subsemiring.
theorem
subsemiring.pow_mem
{R : Type u}
[semiring R]
(s : subsemiring R)
{x : R}
(hx : x ∈ s)
(n : ℕ) :
theorem
subsemiring.nsmul_mem
{R : Type u}
[semiring R]
(s : subsemiring R)
{x : R}
(hx : x ∈ s)
(n : ℕ) :
@[instance]
A subsemiring of a semiring inherits a semiring structure
Equations
- s.to_semiring = {add := add_comm_monoid.add s.to_add_submonoid.to_add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero s.to_add_submonoid.to_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := monoid.mul s.to_submonoid.to_monoid, mul_assoc := _, one := monoid.one s.to_submonoid.to_monoid, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[instance]
Equations
- _ = _
@[instance]
A subsemiring of a comm_semiring is a comm_semiring.
Equations
- s.to_comm_semiring = {add := semiring.add s.to_semiring, add_assoc := _, zero := semiring.zero s.to_semiring, zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul s.to_semiring, mul_assoc := _, one := semiring.one s.to_semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[simp]
@[instance]
Equations
- subsemiring.partial_order = {le := λ (s t : subsemiring R), ∀ ⦃x : R⦄, x ∈ s → x ∈ t, lt := partial_order.lt (partial_order.lift coe subsemiring.ext'), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
subsemiring.mem_to_submonoid
{R : Type u}
[semiring R]
{s : subsemiring R}
{x : R} :
x ∈ s.to_submonoid ↔ x ∈ s
@[simp]
theorem
subsemiring.coe_to_submonoid
{R : Type u}
[semiring R]
(s : subsemiring R) :
↑(s.to_submonoid) = ↑s
@[simp]
theorem
subsemiring.mem_to_add_submonoid
{R : Type u}
[semiring R]
{s : subsemiring R}
{x : R} :
x ∈ s.to_add_submonoid ↔ x ∈ s
@[simp]
theorem
subsemiring.coe_to_add_submonoid
{R : Type u}
[semiring R]
(s : subsemiring R) :
↑(s.to_add_submonoid) = ↑s
def
subsemiring.comap
{R : Type u}
{S : Type v}
[semiring R]
[semiring S] :
(R →+* S) → subsemiring S → subsemiring R
The preimage of a subsemiring along a ring homomorphism is a subsemiring.
@[simp]
theorem
subsemiring.coe_comap
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s : subsemiring S)
(f : R →+* S) :
@[simp]
theorem
subsemiring.mem_comap
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{s : subsemiring S}
{f : R →+* S}
{x : R} :
x ∈ subsemiring.comap f s ↔ ⇑f x ∈ s
theorem
subsemiring.comap_comap
{R : Type u}
{S : Type v}
{T : Type w}
[semiring R]
[semiring S]
[semiring T]
(s : subsemiring T)
(g : S →+* T)
(f : R →+* S) :
subsemiring.comap f (subsemiring.comap g s) = subsemiring.comap (g.comp f) s
def
subsemiring.map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S] :
(R →+* S) → subsemiring R → subsemiring S
The image of a subsemiring along a ring homomorphism is a subsemiring.
@[simp]
theorem
subsemiring.coe_map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(s : subsemiring R) :
@[simp]
theorem
subsemiring.mem_map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
{s : subsemiring R}
{y : S} :
theorem
subsemiring.map_map
{R : Type u}
{S : Type v}
{T : Type w}
[semiring R]
[semiring S]
[semiring T]
(s : subsemiring R)
(g : S →+* T)
(f : R →+* S) :
subsemiring.map g (subsemiring.map f s) = subsemiring.map (g.comp f) s
theorem
subsemiring.map_le_iff_le_comap
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
{s : subsemiring R}
{t : subsemiring S} :
subsemiring.map f s ≤ t ↔ s ≤ subsemiring.comap f t
theorem
subsemiring.gc_map_comap
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
def
ring_hom.srange
{R : Type u}
{S : Type v}
[semiring R]
[semiring S] :
(R →+* S) → subsemiring S
The range of a ring homomorphism is a subsemiring.
Equations
- f.srange = subsemiring.map f ⊤
@[instance]
Equations
- subsemiring.has_bot = {bot := (nat.cast_ring_hom R).srange}
@[instance]
Equations
@[instance]
The inf of two subsemirings is their intersection.
@[simp]
@[simp]
@[instance]
Equations
- subsemiring.has_Inf = {Inf := λ (s : set (subsemiring R)), subsemiring.mk' (⋂ (t : subsemiring R) (H : t ∈ s), ↑t) (⨅ (t : subsemiring R) (H : t ∈ s), t.to_submonoid) _ (⨅ (t : subsemiring R) (H : t ∈ s), t.to_add_submonoid) _}
@[simp]
theorem
subsemiring.coe_Inf
{R : Type u}
[semiring R]
(S : set (subsemiring R)) :
↑(has_Inf.Inf S) = ⋂ (s : subsemiring R) (H : s ∈ S), ↑s
theorem
subsemiring.mem_Inf
{R : Type u}
[semiring R]
{S : set (subsemiring R)}
{x : R} :
x ∈ has_Inf.Inf S ↔ ∀ (p : subsemiring R), p ∈ S → x ∈ p
@[simp]
theorem
subsemiring.Inf_to_submonoid
{R : Type u}
[semiring R]
(s : set (subsemiring R)) :
(has_Inf.Inf s).to_submonoid = ⨅ (t : subsemiring R) (H : t ∈ s), t.to_submonoid
@[simp]
theorem
subsemiring.Inf_to_add_submonoid
{R : Type u}
[semiring R]
(s : set (subsemiring R)) :
(has_Inf.Inf s).to_add_submonoid = ⨅ (t : subsemiring R) (H : t ∈ s), t.to_add_submonoid
@[instance]
Subsemirings of a semiring form a complete lattice.
Equations
- subsemiring.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf subsemiring.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := ⊤, le_top := _, bot := ⊥, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), Inf := complete_lattice.Inf (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
The subsemiring generated by a set.
Equations
- subsemiring.closure s = has_Inf.Inf {S : subsemiring R | s ⊆ ↑S}
theorem
subsemiring.mem_closure
{R : Type u}
[semiring R]
{x : R}
{s : set R} :
x ∈ subsemiring.closure s ↔ ∀ (S : subsemiring R), s ⊆ ↑S → x ∈ S
@[simp]
theorem
subsemiring.subset_closure
{R : Type u}
[semiring R]
{s : set R} :
s ⊆ ↑(subsemiring.closure s)
The subsemiring generated by a set includes the set.
@[simp]
theorem
subsemiring.closure_le
{R : Type u}
[semiring R]
{s : set R}
{t : subsemiring R} :
subsemiring.closure s ≤ t ↔ s ⊆ ↑t
A subsemiring S includes closure s if and only if it includes s.
theorem
subsemiring.closure_mono
{R : Type u}
[semiring R]
⦃s t : set R⦄ :
s ⊆ t → subsemiring.closure s ≤ subsemiring.closure t
Subsemiring closure of a set is monotone in its argument: if s ⊆ t,
then closure s ≤ closure t.
theorem
subsemiring.closure_eq_of_le
{R : Type u}
[semiring R]
{s : set R}
{t : subsemiring R} :
s ⊆ ↑t → t ≤ subsemiring.closure s → subsemiring.closure s = t
theorem
subsemiring.closure_induction
{R : Type u}
[semiring R]
{s : set R}
{p : R → Prop}
{x : R} :
x ∈ subsemiring.closure s → (∀ (x : R), x ∈ s → p x) → p 0 → p 1 → (∀ (x y : R), p x → p y → p (x + y)) → (∀ (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.
closure forms a Galois insertion with the coercion to set.
Equations
- subsemiring.gi R = {choice := λ (s : set R) (_x : ↑(subsemiring.closure s) ≤ s), subsemiring.closure s, gc := _, le_l_u := _, choice_eq := _}
Closure of a subsemiring S equals S.
@[simp]
@[simp]
theorem
subsemiring.closure_union
{R : Type u}
[semiring R]
(s t : set R) :
subsemiring.closure (s ∪ t) = subsemiring.closure s ⊔ subsemiring.closure t
theorem
subsemiring.closure_Union
{R : Type u}
[semiring R]
{ι : Sort u_1}
(s : ι → set R) :
subsemiring.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subsemiring.closure (s i)
theorem
subsemiring.closure_sUnion
{R : Type u}
[semiring R]
(s : set (set R)) :
subsemiring.closure (⋃₀s) = ⨆ (t : set R) (H : t ∈ s), subsemiring.closure t
theorem
subsemiring.map_sup
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s t : subsemiring R)
(f : R →+* S) :
subsemiring.map f (s ⊔ t) = subsemiring.map f s ⊔ subsemiring.map f t
theorem
subsemiring.map_supr
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{ι : Sort u_1}
(f : R →+* S)
(s : ι → subsemiring R) :
subsemiring.map f (supr s) = ⨆ (i : ι), subsemiring.map f (s i)
theorem
subsemiring.comap_inf
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s t : subsemiring S)
(f : R →+* S) :
subsemiring.comap f (s ⊓ t) = subsemiring.comap f s ⊓ subsemiring.comap f t
theorem
subsemiring.comap_infi
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{ι : Sort u_1}
(f : R →+* S)
(s : ι → subsemiring S) :
subsemiring.comap f (infi s) = ⨅ (i : ι), subsemiring.comap f (s i)
@[simp]
theorem
subsemiring.map_bot
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
subsemiring.map f ⊥ = ⊥
@[simp]
theorem
subsemiring.comap_top
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
subsemiring.comap f ⊤ = ⊤
def
subsemiring.prod
{R : Type u}
{S : Type v}
[semiring R]
[semiring S] :
subsemiring R → subsemiring S → subsemiring (R × S)
Given subsemirings s, t of semirings R, S respectively, s.prod t is s × t
as a subsemiring of R × S.
theorem
subsemiring.coe_prod
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s : subsemiring R)
(t : subsemiring S) :
theorem
subsemiring.mem_prod
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{s : subsemiring R}
{t : subsemiring S}
{p : R × S} :
theorem
subsemiring.prod_mono
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
⦃s₁ s₂ : subsemiring R⦄
(hs : s₁ ≤ s₂)
⦃t₁ t₂ : subsemiring S⦄ :
theorem
subsemiring.prod_mono_right
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s : subsemiring R) :
monotone (λ (t : subsemiring S), s.prod t)
theorem
subsemiring.prod_mono_left
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(t : subsemiring S) :
monotone (λ (s : subsemiring R), s.prod t)
theorem
subsemiring.prod_top
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s : subsemiring R) :
s.prod ⊤ = subsemiring.comap (ring_hom.fst R S) s
theorem
subsemiring.top_prod
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s : subsemiring S) :
⊤.prod s = subsemiring.comap (ring_hom.snd R S) s
def
subsemiring.prod_equiv
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s : subsemiring R)
(t : subsemiring S) :
Product of subsemirings is isomorphic to their product as monoids.
theorem
subsemiring.mem_supr_of_directed
{R : Type u}
[semiring R]
{ι : Sort u_1}
[hι : nonempty ι]
{S : ι → subsemiring R}
(hS : directed has_le.le S)
{x : R} :
theorem
subsemiring.coe_supr_of_directed
{R : Type u}
[semiring R]
{ι : Sort u_1}
[hι : nonempty ι]
{S : ι → subsemiring R} :
theorem
subsemiring.mem_Sup_of_directed_on
{R : Type u}
[semiring R]
{S : set (subsemiring R)}
(Sne : S.nonempty)
(hS : directed_on has_le.le S)
{x : R} :
x ∈ has_Sup.Sup S ↔ ∃ (s : subsemiring R) (H : s ∈ S), x ∈ s
theorem
subsemiring.coe_Sup_of_directed_on
{R : Type u}
[semiring R]
{S : set (subsemiring R)} :
S.nonempty → directed_on has_le.le S → (↑(has_Sup.Sup S) = ⋃ (s : subsemiring R) (H : s ∈ S), ↑s)
def
ring_hom.cod_srestrict
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(s : subsemiring S) :
Restriction of a ring homomorphism to a subsemiring of the codomain.
Restriction of a ring homomorphism to its range iterpreted as a subsemiring.
Equations
- f.srange_restrict = f.cod_srestrict f.srange _
@[simp]
theorem
ring_hom.coe_srange_restrict
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : R) :
↑(⇑(f.srange_restrict) x) = ⇑f x
theorem
ring_hom.srange_top_of_surjective
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
function.surjective ⇑f → f.srange = ⊤
The range of a surjective ring homomorphism is the whole of the codomain.
theorem
ring_hom.sclosure_preimage_le
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(s : set S) :
subsemiring.closure (⇑f ⁻¹' s) ≤ subsemiring.comap f (subsemiring.closure s)
theorem
ring_hom.map_sclosure
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(s : set R) :
subsemiring.map f (subsemiring.closure s) = subsemiring.closure (⇑f '' s)
The image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set.
The ring homomorphism associated to an inclusion of subsemirings.
Equations
- subsemiring.inclusion h = ↑(S.subtype.cod_srestrict T _)
@[simp]
@[simp]
theorem
subsemiring.range_fst
{R : Type u}
{S : Type v}
[semiring R]
[semiring S] :
(ring_hom.fst R S).srange = ⊤
@[simp]
theorem
subsemiring.range_snd
{R : Type u}
{S : Type v}
[semiring R]
[semiring S] :
(ring_hom.snd R S).srange = ⊤
@[simp]
theorem
subsemiring.prod_bot_sup_bot_prod
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(s : subsemiring R)
(t : subsemiring S) :
Makes the identity isomorphism from a proof two subsemirings of a multiplicative monoid are equal.
Equations
- ring_equiv.subsemiring_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}