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 RingTheory.Adjoin
.
- carrier : Set A
- one_mem' : 1 ∈ s.carrier
- zero_mem' : 0 ∈ s.carrier
- algebraMap_mem' : ∀ (r : R), ↑(algebraMap R A) r ∈ s.carrier
The image of
algebraMap
is contained in the underlying set of the subalgebra
A subalgebra is a sub(semi)ring that includes the range of algebraMap
.
Instances For
Copy of a subalgebra with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Instances For
The projection from a subalgebra of A
to an additive submonoid of A
.
Instances For
A subalgebra over a ring is also a Subring
.
Instances For
Subalgebra
s inherit structure from their Subsemiring
/ Semiring
coercions.
The forgetful map from Subalgebra
to Submodule
as an OrderEmbedding
Instances For
Subalgebra
s inherit structure from their Submodule
coercions.
Embedding of a subalgebra into the algebra.
Instances For
Linear equivalence between S : Submodule R A
and S
. Though these types are equal,
we define it as a LinearEquiv
to avoid type equalities.
Instances For
Transport a subalgebra via an algebra homomorphism.
Instances For
Preimage of a subalgebra under an algebra homomorphism.
Instances For
A submodule containing 1
and closed under multiplication is a subalgebra.
Instances For
Range of an AlgHom
as a subalgebra.
Instances For
Restrict the codomain of an AlgHom
f
to f.range
.
This is the bundled version of Set.rangeFactorization
.
Instances For
The equalizer of two R-algebra homomorphisms
Instances For
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.
Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.
This is a computable alternative to AlgEquiv.ofInjective
.
Instances For
Restrict an injective algebra homomorphism to an algebra isomorphism
Instances For
Restrict an algebra homomorphism between fields to an algebra isomorphism
Instances For
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
Instances For
The minimal subalgebra that includes s
.
Instances For
Galois insertion between adjoin
and coe
.
Instances For
AlgHom
to ⊤ : Subalgebra R A
.
Instances For
The bottom subalgebra is isomorphic to the base ring.
Instances For
The top subalgebra is isomorphic to the algebra.
This is the algebra version of Submodule.topEquiv
.
Instances For
The map S → T
when S
is a subalgebra contained in the subalgebra T
.
This is the subalgebra version of Submodule.ofLe
, or Subring.inclusion
Instances For
Two subalgebras that are equal are also equivalent as algebras.
This is the Subalgebra
version of LinearEquiv.ofEq
and Equiv.Set.ofEq
.
Instances For
The product of two subalgebras is a subalgebra.
Instances For
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.
Instances For
Actions by Subalgebra
s #
These are just copies of the definitions about Subsemiring
starting from
Subring.mulAction
.
The action by a subalgebra is the action by the underlying algebra.
Note that this provides IsScalarTower S R R
which is needed by smul_mul_assoc
.
The action by a subalgebra is the action by the underlying algebra.
The action by a subalgebra is the action by the underlying algebra.
The action by a subalgebra is the action by the underlying algebra.
The action by a subalgebra is the action by the underlying algebra.
The action by a subalgebra is the action by the underlying algebra.
The action by a subalgebra is the action by the underlying algebra.
The center of an algebra is the set of elements which commute with every element. They form a subalgebra.
Instances For
The centralizer of a set as a subalgebra.
Instances For
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
sᵢ ^ n • x ∈ S'
for some n
for each sᵢ
.
A subsemiring is an ℕ
-subalgebra.
Instances For
A subring is a ℤ
-subalgebra.