Algebra over Commutative Semiring #
In this file we define algebra
s over commutative (semi)rings, algebra homomorphisms alg_hom
,
algebra equivalences alg_equiv
. We also define usual operations on alg_hom
s
(id
, comp
).
subalgebra
s are defined in algebra.algebra.subalgebra
.
If S
is an R
-algebra and A
is an S
-algebra then algebra.comap.algebra R S A
can be used
to provide A
with a structure of an R
-algebra. Other than that, algebra.comap
is now
deprecated and replaced with is_scalar_tower
.
For the category of R
-algebras, denoted Algebra R
, see the file
algebra/category/Algebra/basic.lean
.
Notations #
A →ₐ[R] B
:R
-algebra homomorphism fromA
toB
.A ≃ₐ[R] B
:R
-algebra equivalence fromA
toB
.
- to_has_scalar : has_scalar R A
- to_ring_hom : R →+* A
- commutes' : ∀ (r : R) (x : A), (algebra.to_ring_hom.to_fun r) * x = x * algebra.to_ring_hom.to_fun r
- smul_def' : ∀ (r : R) (x : A), r • x = (algebra.to_ring_hom.to_fun r) * x
Given a commutative (semi)ring R
, an R
-algebra is a (possibly noncommutative)
(semi)ring A
endowed with a morphism of rings R →+* A
which lands in the
center of A
.
For convenience, this typeclass extends has_scalar R A
where the scalar action must
agree with left multiplication by the image of the structure morphism.
Given an algebra R A
instance, the structure morphism R →+* A
is denoted algebra_map R A
.
Instances
- ideal.quotient_algebra
- normed_algebra.to_algebra
- algebra.id
- algebra.prod.algebra
- algebra.of_subsemiring
- algebra.of_subring
- opposite.algebra
- module.endomorphism_algebra
- matrix_algebra
- algebra.comap.algebra'
- algebra.comap.algebra
- rat.algebra_rat
- algebra_nat
- algebra_int
- pi.algebra
- subalgebra.algebra
- subalgebra.to_algebra
- monoid_algebra.algebra
- add_monoid_algebra.algebra
- free_algebra.algebra
- Algebra.is_algebra
- mv_polynomial.algebra
- ideal.quotient.algebra
- Algebra.algebra_obj
- Algebra.limit_algebra
- ring_quot.algebra
- polynomial.algebra_of_algebra
- triv_sq_zero_ext.algebra
- tensor_algebra.algebra
- universal_enveloping_algebra.algebra
- zmod.algebra
- nnreal.real.algebra
- continuous_linear_map.algebra
- set_of.algebra
- continuous_map_algebra
- real_maps_algebra
- complex.algebra_over_reals
- bounded_continuous_function.algebra
- mv_power_series.algebra
- power_series.algebra
- localization_map.algebra
- localization.algebra
- fraction_ring.algebra
- adjoin_root.algebra
- polynomial.splitting_field_aux.algebra
- polynomial.splitting_field_aux.algebra'
- polynomial.splitting_field_aux.algebra''
- polynomial.splitting_field_aux.algebra'''
- polynomial.splitting_field.algebra
- quaternion_algebra.algebra
- quaternion.algebra
- Module.Mon_Module_equivalence_Algebra.Mon_.X.algebra
- subfield.to_algebra
- intermediate_field.algebra
- intermediate_field.to_algebra
- intermediate_field.lift2_alg
- intermediate_field.algebra_over_bot
- algebraic_closure.adjoin_monic.algebra
- algebraic_closure.step.algebra_succ
- algebraic_closure.step.algebra
- algebraic_closure.algebra_of_step
- algebraic_closure.algebra
- fixed_points.algebra
- intermediate_field.fixed_field.algebra
- polynomial.gal.algebra
- times_cont_mdiff_map.algebra
- algebra.tensor_product.tensor_product.algebra
- matrix.algebra
- exterior_algebra.algebra
- clifford_algebra.algebra
- valuation.algebra
Embedding R →+* A
given by algebra
structure.
Equations
Creating an algebra from a morphism to the center of a semiring.
Equations
- i.to_algebra' h = {to_has_scalar := {smul := λ (c : R) (x : S), (⇑i c) * x}, to_ring_hom := i, commutes' := h, smul_def' := _}
Creating an algebra from a morphism to a commutative semiring.
Equations
- i.to_algebra = i.to_algebra' _
Let R
be a commutative semiring, let A
be a semiring with a semimodule R
structure.
If (r • 1) * x = x * (r • 1) = r • x
for all r : R
and x : A
, then A
is an algebra
over R
.
Equations
- algebra.of_semimodule' h₁ h₂ = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := λ (r : R), r • 1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
Let R
be a commutative semiring, let A
be a semiring with a semimodule R
structure.
If (r • x) * y = x * (r • y) = r • (x * y)
for all r : R
and x y : A
, then A
is an algebra
over R
.
Equations
- algebra.of_semimodule h₁ h₂ = algebra.of_semimodule' _ _
To prove two algebra structures on a fixed [comm_semiring R] [semiring A]
agree,
it suffices to check the algebra_map
s agree.
Equations
- algebra.to_semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := algebra.to_has_scalar _inst_4, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
The canonical ring homomorphism algebra_map R A : R →* A
for any R
-algebra A
,
packaged as an R
-linear map.
Equations
- algebra.linear_map R A = {to_fun := (algebra_map R A).to_fun, map_add' := _, map_smul' := _}
Equations
- algebra.id R = (ring_hom.id R).to_algebra
Equations
- algebra.prod.algebra R A B = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := ((algebra_map R A).prod (algebra_map R B)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
Algebra over a subsemiring.
Algebra over a subring.
Algebra over a set that is closed under the ring operations.
Equations
Explicit characterization of the submonoid map in the case of an algebra.
S
is made explicit to help with type inference
Equations
- algebra.algebra_map_submonoid S M = submonoid.map ↑(algebra_map R S) M
A semiring
that is an algebra
over a commutative ring carries a natural ring
structure.
Equations
- algebra.semiring_to_ring R = {add := add_comm_group.add (semimodule.add_comm_monoid_to_add_comm_group R), add_assoc := _, zero := add_comm_group.zero (semimodule.add_comm_monoid_to_add_comm_group R), zero_add := _, add_zero := _, neg := add_comm_group.neg (semimodule.add_comm_monoid_to_add_comm_group R), sub := add_comm_group.sub (semimodule.add_comm_monoid_to_add_comm_group R), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul infer_instance, mul_assoc := _, one := semiring.one infer_instance, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
If algebra_map R A
is injective and A
has no zero divisors,
R
-multiples in A
are zero only if one of the factors is zero.
Cannot be an instance because there is no injective (algebra_map R A)
typeclass.
Equations
- opposite.algebra = {to_has_scalar := {smul := has_scalar.smul (opposite.has_scalar A R)}, to_ring_hom := (algebra_map R A).to_opposite opposite.algebra._proof_1, commutes' := _, smul_def' := _}
Equations
- module.endomorphism_algebra R M = {to_has_scalar := linear_map.has_scalar _, to_ring_hom := {to_fun := λ (r : R), r • linear_map.id, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
Equations
- matrix_algebra n R = {to_has_scalar := matrix.has_scalar (comm_semiring.to_semiring R), to_ring_hom := {to_fun := (matrix.scalar n).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
- to_fun : A → B
- map_one' : c.to_fun 1 = 1
- map_mul' : ∀ (x y : A), c.to_fun (x * y) = (c.to_fun x) * c.to_fun y
- map_zero' : c.to_fun 0 = 0
- map_add' : ∀ (x y : A), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- commutes' : ∀ (r : R), c.to_fun (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
Defining the homomorphism in the category R-Alg.
Equations
- alg_hom.coe_ring_hom = {coe := alg_hom.to_ring_hom _inst_7}
Identity map as an alg_hom
.
- to_fun : A → B
- inv_fun : B → A
- left_inv : function.left_inverse c.inv_fun c.to_fun
- right_inv : function.right_inverse c.inv_fun c.to_fun
- map_mul' : ∀ (x y : A), c.to_fun (x * y) = (c.to_fun x) * c.to_fun y
- map_add' : ∀ (x y : A), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- commutes' : ∀ (r : R), c.to_fun (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
An equivalence of algebras is an equivalence of rings commuting with the actions of scalars.
Equations
- alg_equiv.has_coe_to_fun = {F := λ (x : A₁ ≃ₐ[R] A₂), A₁ → A₂, coe := alg_equiv.to_fun _inst_6}
Equations
- alg_equiv.has_coe_to_ring_equiv = {coe := alg_equiv.to_ring_equiv _inst_6}
Interpret an algebra equivalence as an algebra homomorphism.
This definition is included for symmetry with the other to_*_hom
projections.
The simp
normal form is to use the coercion of the has_coe_to_alg_hom
instance.
Equations
- alg_equiv.has_coe_to_alg_hom = {coe := alg_equiv.to_alg_hom _inst_6}
Equations
- alg_equiv.inhabited = {default := 1}
Algebra equivalences are reflexive.
Equations
Algebra equivalences are symmetric.
See Note [custom simps projection]
Equations
- alg_equiv.simps.inv_fun e = ⇑(e.symm)
Algebra equivalences are transitive.
Equations
- e₁.trans e₂ = {to_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).to_fun, inv_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
If A₁
is equivalent to A₁'
and A₂
is equivalent to A₂'
, then the type of maps
A₁ →ₐ[R] A₂
is equivalent to the type of maps A₁' →ₐ[R] A₂'
.
Equations
- e₁.arrow_congr e₂ = {to_fun := λ (f : A₁ →ₐ[R] A₂), (e₂.to_alg_hom.comp f).comp e₁.symm.to_alg_hom, inv_fun := λ (f : A₁' →ₐ[R] A₂'), (e₂.symm.to_alg_hom.comp f).comp e₁.to_alg_hom, left_inv := _, right_inv := _}
If an algebra morphism has an inverse, it is a algebra isomorphism.
Promotes a bijective algebra homomorphism to an algebra equivalence.
Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence.
Interpret an algebra equivalence as a linear map.
Equations
Upgrade a linear equivalence to an algebra equivalence, given that it distributes over multiplication and action of scalars.
Equations
- alg_equiv.aut = {mul := λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := alg_equiv.symm _inst_5, div := div_inv_monoid.div._default (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 1 alg_equiv.aut._proof_5 alg_equiv.aut._proof_6 alg_equiv.symm, div_eq_mul_inv := _, mul_left_inv := _}
matrix
section #
Specialize matrix.one_map
and matrix.zero_map
to alg_hom
and alg_equiv
.
TODO: there should be a way to avoid restating these for each foo_hom
.
A version of matrix.one_map
where f
is an alg_hom
.
A version of matrix.one_map
where f
is an alg_equiv
.
comap R S A
is a type alias for A
, and has an R-algebra structure defined on it
when algebra R S
and algebra S A
. If S
is an R
-algebra and A
is an S
-algebra then
algebra.comap.algebra R S A
can be used to provide A
with a structure of an R
-algebra.
Other than that, algebra.comap
is now deprecated and replaced with is_scalar_tower
.
Equations
- algebra.comap R S A = A
Equations
- algebra.comap.inhabited R S A = h
Equations
- algebra.comap.semiring R S A = h
Equations
- algebra.comap.ring R S A = h
Equations
- algebra.comap.comm_semiring R S A = h
Equations
- algebra.comap.comm_ring R S A = h
Equations
- algebra.comap.algebra' R S A = h
Identity homomorphism A →ₐ[S] comap R S A
.
Equations
- algebra.comap.to_comap R S A = alg_hom.id S A
Identity homomorphism comap R S A →ₐ[S] A
.
Equations
- algebra.comap.of_comap R S A = alg_hom.id S A
R ⟶ S
induces S-Alg ⥤ R-Alg
Equations
- algebra.comap.algebra R S A = {to_has_scalar := {smul := λ (r : R) (x : algebra.comap R S A), ⇑(algebra_map R S) r • x}, to_ring_hom := {to_fun := ((algebra_map S A).comp (algebra_map R S)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
Embedding of S
into comap R S A
.
R ⟶ S induces S-Alg ⥤ R-Alg
Equations
- rat.algebra_rat = (rat.cast_hom α).to_algebra' rat.algebra_rat._proof_1
algebra_map
as an alg_hom
.
The multiplication in an algebra is a bilinear map.
The multiplication on the left in an algebra is a linear map.
Equations
- algebra.lmul_left R r = ⇑(algebra.lmul R A) r
The multiplication on the right in an algebra is a linear map.
Equations
- algebra.lmul_right R r = ⇑((algebra.lmul R A).to_linear_map.flip) r
Simultaneous multiplication on the left and right is a linear map.
Equations
- algebra.lmul_left_right R vw = (algebra.lmul_right R vw.snd).comp (algebra.lmul_left R vw.fst)
The multiplication map on an algebra, as an R
-linear map from A ⊗[R] A
to A
.
Equations
Equations
- algebra.linear_map.semimodule' R M S = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (s : S) (f : M →ₗ[R] S), ⇑(⇑(linear_map.llcomp R M S S) (⇑(algebra.lmul R S) s)) f}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Semiring ⥤ ℕ-Alg
Equations
- algebra_nat R = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := nat.cast_ring_hom R _inst_1, commutes' := _, smul_def' := _}
Ring ⥤ ℤ-Alg
Equations
- algebra_int R = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := int.cast_ring_hom R _inst_1, commutes' := _, smul_def' := _}
The R-algebra structure on Π i : I, A i
when each A i
is an R-algebra.
We couldn't set this up back in algebra.pi_instances
because this file imports it.
Equations
- pi.algebra I f α = {to_has_scalar := pi.has_scalar (λ (i : I), mul_action.to_has_scalar), to_ring_hom := {to_fun := (pi.ring_hom (λ (i : I), algebra_map α (f i))).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
A
-linearly coerce a R
-linear map from M
to A
to a function, given an algebra A
over
a commutative semiring R
and M
a semimodule over R
.
Equations
- linear_map.lto_fun R M A = {to_fun := linear_map.to_fun algebra.to_semimodule, map_add' := _, map_smul' := _}
Warning: use this type synonym judiciously!
The preferred way of working with an A
-module M
as R
-module (where A
is an R
-algebra),
is by [module R M] [module A M] [is_scalar_tower R A M]
.
When M
is a module over a ring A
, and A
is an algebra over R
, then M
inherits a
module structure over R
, provided as a type synonym module.restrict_scalars R A M := M
.
Equations
- restrict_scalars R A M = M
Equations
- restrict_scalars.inhabited R A M = I
Equations
- restrict_scalars.add_comm_monoid R A M = I
Equations
- restrict_scalars.add_comm_group R A M = I
Equations
- restrict_scalars.module_orig R A M = I
When M
is a module over a ring A
, and A
is an algebra over R
, then M
inherits a
module structure over R
.
The preferred way of setting this up is [module R M] [module A M] [is_scalar_tower R A M]
.
Equations
- restrict_scalars.semimodule R A M = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (c : R) (x : restrict_scalars R A M), ⇑(algebra_map R A) c • x}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Equations
- submodule.restricted_module R A M V = restrict_scalars.semimodule R A ↥V
V.restrict_scalars R
is the R
-submodule of the R
-module given by restriction of scalars,
corresponding to V
, an S
-submodule of the original S
-module.
If A
is an R
-algebra, then the R
-module generated by a set X
is included in the
A
-module generated by X
.
If A
is an R
-algebra such that the induced morhpsim R →+* A
is surjective, then the
R
-module generated by a set X
equals the A
-module generated by X
.