Subalgebras over Commutative Semiring #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
- mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ self.carrier
A subalgebra is a sub(semi)ring that includes the range of algebra_map
.
Instances for subalgebra
- subalgebra.has_sizeof_inst
- subalgebra.set_like
- subalgebra.subsemiring_class
- subalgebra.smul_mem_class
- subalgebra.subring_class
- algebra.subalgebra.complete_lattice
- algebra.subalgebra.inhabited
- subalgebra.subsingleton_of_subsingleton
- subalgebra.unique
- subalgebra.has_involutive_star
- polynomial.subalgebra.nontrivial
- continuous_map.subsingleton_subalgebra
- mv_power_series.subalgebra.nontrivial
- power_series.subalgebra.nontrivial
- hahn_series.subalgebra.nontrivial
- Algebra.has_coe
Reinterpret a subalgebra
as a subsemiring
.
Equations
- subalgebra.set_like = {coe := subalgebra.carrier _inst_3, coe_injective' := _}
Copy of a subalgebra with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Equations
The projection from a subalgebra of A
to an additive submonoid of A
.
Equations
The projection from a subalgebra of A
to a submonoid of A
.
Equations
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
Equations
Equations
Equations
The forgetful map from subalgebra
to submodule
as an order_embedding
Equations
- subalgebra.to_submodule = {to_embedding := {to_fun := λ (S : subalgebra R A), {carrier := ↑S, add_mem' := _, zero_mem' := _, smul_mem' := _}, inj' := _}, map_rel_iff' := _}
subalgebra
s inherit structure from their submodule
coercions.
Equations
Equations
- S.algebra' = {to_has_smul := smul_zero_class.to_has_smul smul_with_zero.to_smul_zero_class, to_ring_hom := {to_fun := ((algebra_map R' A).cod_restrict S _).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
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
Transport a subalgebra via an algebra homomorphism.
Equations
- subalgebra.map f S = {carrier := (subsemiring.map ↑f S.to_subsemiring).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
Preimage of a subalgebra under an algebra homomorphism.
Equations
- subalgebra.comap f S = {carrier := (subsemiring.comap ↑f S.to_subsemiring).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
A submodule containing 1
and closed under multiplication is a subalgebra.
Equations
- p.to_subalgebra h_one h_mul = {carrier := p.carrier, mul_mem' := h_mul, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
Range of an alg_hom
as a subalgebra.
Equations
Instances for ↥alg_hom.range
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
The range of a morphism of algebras is a fintype, if the domain is a fintype.
Note that this instance can cause a diamond with subtype.fintype
if B
is also a fintype.
Equations
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
Given an equivalence e : A ≃ₐ[R] B
of R
-algebras and a subalgebra S
of A
,
subalgebra_map
is the induced equivalence between S
and S.map e
Equations
- e.subalgebra_map S = {to_fun := (e.to_ring_equiv.subsemiring_map S.to_subsemiring).to_fun, inv_fun := (e.to_ring_equiv.subsemiring_map S.to_subsemiring).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
The minimal subalgebra that includes s
.
Equations
- algebra.adjoin R s = {carrier := (subsemiring.closure (set.range ⇑(algebra_map R A) ∪ s)).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_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).copy s _, gc := _, le_l_u := _, choice_eq := _}
Equations
alg_hom
to ⊤ : subalgebra R A
.
Equations
- algebra.to_top = (alg_hom.id R A).cod_restrict ⊤ algebra.to_top._proof_1
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 algebra.
This is the algebra version of submodule.top_equiv
.
Equations
- subalgebra.top_equiv = alg_equiv.of_alg_hom ⊤.val algebra.to_top subalgebra.top_equiv._proof_1 subalgebra.top_equiv._proof_2
Equations
The map S → T
when S
is a subalgebra contained in the subalgebra T
.
This is the subalgebra version of submodule.of_le
, or subring.inclusion
Equations
- subalgebra.inclusion h = {to_fun := set.inclusion h, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
Two subalgebras that are equal are also equivalent as algebras.
This is the subalgebra
version of linear_equiv.of_eq
and equiv.set.of_eq
.
The product of two subalgebras is a subalgebra.
Define an algebra homomorphism on a directed supremum of subalgebras by defining it on each subalgebra, and proving that it agrees on the intersection of subalgebras.
Actions by subalgebra
s #
These are just copies of the definitions about subsemiring
starting from
subring.mul_action
.
The action by a subalgebra is the action by the underlying algebra.
Equations
Note that this provides is_scalar_tower S R R
which is needed by smul_mul_assoc
.
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The center of an algebra is the set of elements which commute with every element. They form a subalgebra.
Equations
- subalgebra.center R A = {carrier := (subsemiring.center A).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
Instances for ↥subalgebra.center
The centralizer of a set as a subalgebra.
Equations
- subalgebra.centralizer R s = {carrier := (subsemiring.centralizer s).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
Suppose we are given ∑ i, lᵢ * sᵢ = 1
in S
, and S'
a subalgebra of S
that contains
lᵢ
and sᵢ
. To check that an x : S
falls in S'
, we only need to show that
r ^ n • x ∈ M'
for some n
for each r : s
.
A subsemiring is a ℕ
-subalgebra.
Equations
- subalgebra_of_subsemiring S = {carrier := S.carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
A subring is a ℤ
-subalgebra.
Equations
- subalgebra_of_subring S = {carrier := S.carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}