Adjoining elements to form subalgebras #
This file develops the basic theory of subalgebras of an R-algebra generated
by a set of elements. A basic interface for adjoin
is set up.
Tags #
adjoin, algebra
Induction principle for the algebra generated by a set s
: show that p x y
holds for any
x y ∈ adjoin R s
given that it holds for x y ∈ s
and that it satisfies a number of
natural properties.
The difference with Algebra.adjoin_induction
is that this acts on the subtype.
If all elements of s : Set A
commute pairwise, then adjoin R s
is a commutative
semiring.
Equations
- Algebra.adjoinCommSemiringOfComm R hcomm = CommSemiring.mk ⋯
Instances For
If all elements of s : Set A
commute pairwise, then adjoin R s
is a commutative
ring.
Equations
- Algebra.adjoinCommRingOfComm R hcomm = CommRing.mk ⋯
Instances For
Two algebra morphisms are equal on Algebra.span s
iff they are equal on s
The ℕ
-algebra equivalence between Subsemiring.closure s
and Algebra.adjoin ℕ s
given
by the identity map.
Equations
- Subsemiring.closureEquivAdjoinNat s = (subalgebraOfSubsemiring (Subsemiring.closure s)).equivOfEq (Algebra.adjoin ℕ s) ⋯
Instances For
The ℤ
-algebra equivalence between Subring.closure s
and Algebra.adjoin ℤ s
given by
the identity map.
Equations
- Subring.closureEquivAdjoinInt s = (subalgebraOfSubring (Subring.closure s)).equivOfEq (Algebra.adjoin ℤ s) ⋯
Instances For
If K / E / F
is a ring extension tower, L
is a submonoid of K / F
which is generated by
S
as an F
-module, then E[L]
is generated by S
as an E
-module.
If K / E / F
is a ring extension tower, L
is a subalgebra of K / F
which is generated by
S
as an F
-module, then E[L]
is generated by S
as an E
-module.
If K / E / F
is a ring extension tower, L
is a subalgebra of K / F
,
then E[L]
is generated by any basis of L / F
as an E
-module.
If E / L / F
and E / L' / F
are two ring extension towers, L ≃ₐ[F] L'
is an isomorphism
compatible with E / L
and E / L'
, then for any subset S
of E
, L[S]
and L'[S]
are
equal as subalgebras of E / F
.