Subalgebras over Commutative Semiring #
In this file we define subalgebra
s and the usual operations on them (map
, comap
).
More lemmas about adjoin
can be found in ring_theory.adjoin
.
- carrier : set A
- one_mem' : 1 ∈ c.carrier
- mul_mem' : ∀ {a b : A}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
- zero_mem' : 0 ∈ c.carrier
- add_mem' : ∀ {a b : A}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
- algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ c.carrier
A subalgebra is a sub(semi)ring that includes the range of algebra_map
.
Reinterpret a subalgebra
as a subsemiring
.
Equations
- subalgebra.has_mem = {mem := λ (x : A) (S : subalgebra R A), x ∈ ↑S}
A subalgebra over a ring is also a subring
.
subalgebra
s inherit structure from their subsemiring
/ semiring
coercions.
Equations
Equations
Equations
- S.to_ring = S.to_subring.to_ring
Equations
Equations
Equations
Equations
Equations
Equations
There is no linear_ordered_comm_semiring
.
Equations
Equations
Equations
Embedding of a subalgebra into the algebra.
Convert a subalgebra
to submodule
Equations
- subalgebra.coe_to_submodule = {coe := subalgebra.to_submodule _inst_3}
As submodules, subalgebras are idempotent.
Linear equivalence between S : submodule R A
and S
. Though these types are equal,
we define it as a linear_equiv
to avoid type equalities.
Equations
Equations
- subalgebra.partial_order = {le := λ (S T : subalgebra R A), ↑S ⊆ ↑T, lt := preorder.lt._default (λ (S T : subalgebra R A), ↑S ⊆ ↑T), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Reinterpret an S
-subalgebra as an R
-subalgebra in comap R S A
.
If S
is an R
-subalgebra of A
and T
is an S
-subalgebra of A
,
then T
is an R
-subalgebra of A
.
Transport a subalgebra via an algebra homomorphism.
Preimage of a subalgebra under an algebra homomorphism.
Equations
Range of an alg_hom
as a subalgebra.
Restrict the codomain of an algebra homomorphism.
Restrict the codomain of a alg_hom f
to f.range
.
This is the bundled version of set.range_factorization
.
Equations
- f.range_restrict = f.cod_restrict f.range _
The equalizer of two R-algebra homomorphisms
Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.
This is a computable alternative to alg_equiv.of_injective
.
Restrict an injective algebra homomorphism to an algebra isomorphism
Equations
Restrict an algebra homomorphism between fields to an algebra isomorphism
Equations
The minimal subalgebra that includes s
.
Equations
- algebra.adjoin R s = {carrier := (subsemiring.closure (set.range ⇑(algebra_map R A) ∪ s)).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}
Galois insertion between adjoin
and coe
.
Equations
- algebra.gi = {choice := λ (s : set A) (hs : ↑(algebra.adjoin R s) ≤ s), algebra.adjoin R s, gc := _, le_l_u := _, choice_eq := _}
Equations
The bottom subalgebra is isomorphic to the base ring.
Equations
The bottom subalgebra is isomorphic to the field.
Equations
The top subalgebra is isomorphic to the field.
Equations
- algebra.top_equiv = (alg_equiv.of_bijective algebra.to_top algebra.top_equiv._proof_1).symm
Equations
- subalgebra.unique = {to_inhabited := {default := default (subalgebra R R) algebra.subalgebra.inhabited}, uniq := _}
A subsemiring is a ℕ
-subalgebra.
Equations
- subalgebra_of_subsemiring S = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}
A subring is a ℤ
-subalgebra.
Equations
- subalgebra_of_subring S = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}
A subset closed under the ring operations is a ℤ
-subalgebra.