Algebra over Commutative Semiring (under category)
In this file we define algebra over commutative (semi)rings, algebra homomorphisms alg_hom,
algebra equivalences alg_equiv, and subalgebras. We also define usual operations on alg_homs
(id, comp) and subalgebras (map, comap).
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 replcaed with is_scalar_tower.
Notations
A →ₐ[R] B:R-algebra homomorphism fromAtoB.A ≃ₐ[R] B:R-algebra equivalence fromAtoB.
@[nolint, class]
- 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
The category of R-algebras where R is a commutative ring is the under category R ↓ CRing. In the categorical setting we have a forgetful functor R-Alg ⥤ R-Mod. However here it extends module in order to preserve definitional equality in certain cases.
Instances
- normed_algebra.to_algebra
- algebra.id
- algebra.of_subsemiring
- algebra.of_subring
- module.endomorphism_algebra
- matrix_algebra
- algebra.comap.algebra'
- algebra.comap.algebra
- rat.algebra_rat
- subalgebra.algebra
- subalgebra.to_algebra
- algebra_nat
- algebra_int
- pi.algebra
- Algebra.is_algebra
- Algebra.algebra_obj
- Algebra.limit_algebra
- monoid_algebra.algebra
- add_monoid_algebra.algebra
- mv_polynomial.algebra
- polynomial.algebra_of_algebra
- complex.algebra_over_reals
- continuous_linear_map.algebra
- bounded_continuous_function.algebra
- set_of.algebra
- continuous_map.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
- 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
- algebra.tensor_product.algebra
- matrix.algebra
- tensor_algebra.algebra
- localization_map.algebra
- localization.algebra
- mv_power_series.algebra
- power_series.algebra
Embedding R →+* A given by algebra structure.
Equations
def
ring_hom.to_algebra'
{R : Type u_1}
{S : Type u_2}
[comm_semiring R]
[semiring S]
(i : R →+* S) :
Creating an algebra from a morphism to the center of a semiring.
Creating an algebra from a morphism to a commutative semiring.
Equations
- i.to_algebra = i.to_algebra' _
def
algebra.of_semimodule'
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[semimodule R A] :
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' := _}
def
algebra.of_semimodule
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[semimodule R A] :
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' _ _
theorem
algebra.smul_def''
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R)
(x : A) :
r • x = ⇑(algebra_map R A) r * x
@[ext]
theorem
algebra.algebra_ext
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[semiring A]
(P Q : algebra R A) :
(∀ (r : R), ⇑(algebra_map R A) r = ⇑(algebra_map R A) r) → P = Q
To prove two algebra structures on a fixed [comm_semiring R] [semiring A] agree,
it suffices to check the algebra_maps agree.
@[instance]
def
algebra.to_semimodule
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A] :
semimodule R A
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 := _}
theorem
algebra.smul_def
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R)
(x : A) :
r • x = ⇑(algebra_map R A) r * x
theorem
algebra.algebra_map_eq_smul_one
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
⇑(algebra_map R A) r = r • 1
theorem
algebra.commutes
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R)
(x : A) :
⇑(algebra_map R A) r * x = x * ⇑(algebra_map R A) r
theorem
algebra.left_comm
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R)
(x y : A) :
x * (⇑(algebra_map R A) r * y) = ⇑(algebra_map R A) r * (x * y)
@[simp]
theorem
algebra.mul_smul_comm
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : R)
(x y : A) :
@[simp]
theorem
algebra.smul_mul_assoc
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R)
(x y : A) :
@[instance]
Equations
- algebra.id R = (ring_hom.id R).to_algebra
@[simp]
@[simp]
@[instance]
def
algebra.of_subsemiring
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subsemiring R) :
Algebra over a subsemiring.
@[instance]
def
algebra.of_subring
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
(S : set R)
[is_subring S] :
Algebra over a subring.
Equations
- algebra.of_subring S = {to_has_scalar := {smul := λ (s : ↥S) (x : A), ↑s • x}, to_ring_hom := {to_fun := ((algebra_map R A).comp {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
theorem
algebra.subring_coe_algebra_map_hom
{R : Type u_1}
[comm_ring R]
(S : set R)
[is_subring S] :
algebra_map ↥S R = is_subring.subtype S
theorem
algebra.subring_coe_algebra_map
{R : Type u_1}
[comm_ring R]
(S : set R)
[is_subring S] :
⇑(algebra_map ↥S R) = subtype.val
theorem
algebra.subring_algebra_map_apply
{R : Type u_1}
[comm_ring R]
(S : set R)
[is_subring S]
(x : ↥S) :
⇑(algebra_map ↥S R) x = ↑x
The multiplication in an algebra is a bilinear map.
Equations
- algebra.lmul R A = linear_map.mk₂ R has_mul.mul _ _ _ _
The multiplication on the left in an algebra is a linear map.
Equations
- algebra.lmul_left R A r = ⇑(algebra.lmul R A) r
The multiplication on the right in an algebra is a linear map.
Equations
- algebra.lmul_right R A r = ⇑((algebra.lmul R A).flip) r
def
algebra.lmul_left_right
(R : Type u)
(A : Type w)
[comm_semiring R]
[semiring A]
[algebra R A] :
Simultaneous multiplication on the left and right is a linear map.
Equations
- algebra.lmul_left_right R A vw = (algebra.lmul_right R A vw.snd).comp (algebra.lmul_left R A vw.fst)
@[simp]
theorem
algebra.lmul_apply
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(p q : A) :
⇑(⇑(algebra.lmul R A) p) q = p * q
@[simp]
theorem
algebra.lmul_left_apply
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(p q : A) :
⇑(algebra.lmul_left R A p) q = p * q
@[simp]
theorem
algebra.lmul_right_apply
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(p q : A) :
⇑(algebra.lmul_right R A p) q = q * p
@[simp]
theorem
algebra.lmul_left_right_apply
{R : Type u}
{A : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
(vw : A × A)
(p : A) :
@[instance]
def
module.endomorphism_algebra
(R : Type u)
(M : Type v)
[comm_ring R]
[add_comm_group M]
[module R M] :
Equations
- module.endomorphism_algebra R M = {to_has_scalar := linear_map.has_scalar _inst_3, to_ring_hom := {to_fun := λ (r : R), r • linear_map.id, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
@[instance]
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' := _}
@[nolint]
structure
alg_hom
(R : Type u)
(A : Type v)
(B : Type w)
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
Type (max v w)
- 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.
@[instance]
def
alg_hom.has_coe_to_fun
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
has_coe_to_fun (A →ₐ[R] B)
@[instance]
def
alg_hom.coe_ring_hom
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
Equations
- alg_hom.coe_ring_hom = {coe := alg_hom.to_ring_hom _inst_7}
@[simp]
theorem
alg_hom.coe_mk
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
{f : A → B}
(h₁ : f 1 = 1)
(h₂ : ∀ (x y : A), f (x * y) = f x * f y)
(h₃ : f 0 = 0)
(h₄ : ∀ (x y : A), f (x + y) = f x + f y)
(h₅ : ∀ (r : R), f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r) :
theorem
alg_hom.coe_ring_hom_injective
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
theorem
alg_hom.coe_monoid_hom_injective
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
theorem
alg_hom.coe_add_monoid_hom_injective
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
@[simp]
theorem
alg_hom.commutes
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(φ : A →ₐ[R] B)
(r : R) :
⇑φ (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
theorem
alg_hom.comp_algebra_map
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(φ : A →ₐ[R] B) :
↑φ.comp (algebra_map R A) = algebra_map R B
Identity map as an alg_hom.
@[simp]
theorem
alg_hom.id_apply
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(p : A) :
⇑(alg_hom.id R A) p = p
def
alg_hom.comp
{R : Type u}
{A : Type v}
{B : Type w}
{C : Type u₁}
[comm_semiring R]
[semiring A]
[semiring B]
[semiring C]
[algebra R A]
[algebra R B]
[algebra R C] :
Composition of algebra homeomorphisms.
@[simp]
theorem
alg_hom.comp_id
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(φ : A →ₐ[R] B) :
φ.comp (alg_hom.id R A) = φ
@[simp]
theorem
alg_hom.id_comp
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(φ : A →ₐ[R] B) :
(alg_hom.id R B).comp φ = φ
@[simp]
theorem
alg_hom.to_linear_map_apply
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(φ : A →ₐ[R] B)
(p : A) :
⇑(φ.to_linear_map) p = ⇑φ p
theorem
alg_hom.to_linear_map_inj
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
{φ₁ φ₂ : A →ₐ[R] B} :
φ₁.to_linear_map = φ₂.to_linear_map → φ₁ = φ₂
@[simp]
theorem
alg_hom.comp_to_linear_map
{R : Type u}
{A : Type v}
{B : Type w}
{C : Type u₁}
[comm_semiring R]
[semiring A]
[semiring B]
[semiring C]
[algebra R A]
[algebra R B]
[algebra R C]
(f : A →ₐ[R] B)
(g : B →ₐ[R] C) :
(g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map
theorem
alg_hom.map_prod
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_semiring B]
[algebra R A]
[algebra R B]
(φ : A →ₐ[R] B)
{ι : Type u_1}
(f : ι → A)
(s : finset ι) :
theorem
alg_hom.injective_iff
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[ring A]
[semiring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B) :
@[nolint]
def
alg_equiv.to_mul_equiv
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
@[nolint]
def
alg_equiv.to_equiv
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
structure
alg_equiv
(R : Type u)
(A : Type v)
(B : Type w)
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
Type (max v w)
- 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.
@[nolint]
def
alg_equiv.to_add_equiv
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
@[nolint]
def
alg_equiv.to_ring_equiv
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
@[instance]
def
alg_equiv.has_coe_to_fun
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂] :
has_coe_to_fun (A₁ ≃ₐ[R] A₂)
Equations
- alg_equiv.has_coe_to_fun = {F := λ (x : A₁ ≃ₐ[R] A₂), A₁ → A₂, coe := alg_equiv.to_fun _inst_6}
theorem
alg_equiv.coe_fun_injective
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂] :
function.injective (λ (e : A₁ ≃ₐ[R] A₂), ⇑e)
@[instance]
def
alg_equiv.has_coe_to_ring_equiv
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂] :
Equations
- alg_equiv.has_coe_to_ring_equiv = {coe := alg_equiv.to_ring_equiv _inst_6}
@[simp]
theorem
alg_equiv.mk_apply
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
{to_fun : A₁ → A₂}
{inv_fun : A₂ → A₁}
{left_inv : function.left_inverse inv_fun to_fun}
{right_inv : function.right_inverse inv_fun to_fun}
{map_mul : ∀ (x y : A₁), to_fun (x * y) = to_fun x * to_fun y}
{map_add : ∀ (x y : A₁), to_fun (x + y) = to_fun x + to_fun y}
{commutes : ∀ (r : R), to_fun (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r}
{a : A₁} :
theorem
alg_equiv.coe_ring_equiv_injective
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂] :
function.injective (λ (e : A₁ ≃ₐ[R] A₂), ↑e)
@[simp]
theorem
alg_equiv.commutes
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂)
(r : R) :
⇑e (⇑(algebra_map R A₁) r) = ⇑(algebra_map R A₂) r
@[instance]
def
alg_equiv.has_coe_to_alg_hom
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂] :
theorem
alg_equiv.injective
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂) :
theorem
alg_equiv.surjective
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂) :
theorem
alg_equiv.bijective
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂) :
@[instance]
def
alg_equiv.inhabited
{R : Type u}
{A₁ : Type v}
[comm_semiring R]
[semiring A₁]
[algebra R A₁] :
Equations
- alg_equiv.inhabited = {default := 1}
Algebra equivalences are reflexive.
Equations
@[simp]
theorem
alg_equiv.coe_refl
{R : Type u}
{A₁ : Type v}
[comm_semiring R]
[semiring A₁]
[algebra R A₁] :
↑alg_equiv.refl = alg_hom.id R A₁
def
alg_equiv.symm
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂] :
Algebra equivalences are symmetric.
def
alg_equiv.trans
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
{A₃ : Type u₁}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[semiring A₃]
[algebra R A₁]
[algebra R A₂]
[algebra R A₃] :
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' := _}
@[simp]
theorem
alg_equiv.comp_symm
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂) :
@[simp]
theorem
alg_equiv.symm_comp
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂) :
def
alg_equiv.of_alg_hom
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(f : A₁ →ₐ[R] A₂)
(g : A₂ →ₐ[R] A₁) :
f.comp g = alg_hom.id R A₂ → g.comp f = alg_hom.id R A₁ → (A₁ ≃ₐ[R] A₂)
If an algebra morphism has an inverse, it is a algebra isomorphism.
def
alg_equiv.of_bijective
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(f : A₁ →ₐ[R] A₂) :
function.bijective ⇑f → (A₁ ≃ₐ[R] A₂)
Promotes a bijective algebra homomorphism to an algebra equivalence.
def
alg_equiv.to_linear_equiv
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂] :
Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence.
@[simp]
theorem
alg_equiv.to_linear_equiv_apply
{R : Type u}
{A₁ : Type v}
{A₂ : Type w}
[comm_semiring R]
[semiring A₁]
[semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂)
(x : A₁) :
⇑(e.to_linear_equiv) x = ⇑e x
@[nolint]
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
@[instance]
def
algebra.comap.inhabited
(R : Type u)
(S : Type v)
(A : Type w)
[h : inhabited A] :
inhabited (algebra.comap R S A)
Equations
- algebra.comap.inhabited R S A = h
@[instance]
def
algebra.comap.semiring
(R : Type u)
(S : Type v)
(A : Type w)
[h : semiring A] :
semiring (algebra.comap R S A)
Equations
- algebra.comap.semiring R S A = h
@[instance]
def
algebra.comap.ring
(R : Type u)
(S : Type v)
(A : Type w)
[h : ring A] :
ring (algebra.comap R S A)
Equations
- algebra.comap.ring R S A = h
@[instance]
def
algebra.comap.comm_semiring
(R : Type u)
(S : Type v)
(A : Type w)
[h : comm_semiring A] :
comm_semiring (algebra.comap R S A)
Equations
- algebra.comap.comm_semiring R S A = h
@[instance]
def
algebra.comap.comm_ring
(R : Type u)
(S : Type v)
(A : Type w)
[h : comm_ring A] :
comm_ring (algebra.comap R S A)
Equations
- algebra.comap.comm_ring R S A = h
@[instance]
def
algebra.comap.algebra'
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring S]
[semiring A]
[h : algebra S A] :
algebra S (algebra.comap R S A)
Equations
- algebra.comap.algebra' R S A = h
def
algebra.comap.to_comap
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring S]
[semiring A]
[algebra S A] :
A →ₐ[S] algebra.comap R S A
Identity homomorphism A →ₐ[S] comap R S A.
Equations
- algebra.comap.to_comap R S A = alg_hom.id S A
def
algebra.comap.of_comap
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring S]
[semiring A]
[algebra S A] :
algebra.comap R S A →ₐ[S] A
Identity homomorphism comap R S A →ₐ[S] A.
Equations
- algebra.comap.of_comap R S A = alg_hom.id S A
@[instance]
def
algebra.comap.algebra
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A] :
algebra R (algebra.comap R 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' := _}
def
algebra.to_comap
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A] :
S →ₐ[R] algebra.comap R S A
Embedding of S into comap R S A.
theorem
algebra.to_comap_apply
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
(x : S) :
⇑(algebra.to_comap R S A) x = ⇑(algebra_map S A) x
def
alg_hom.comap
{R : Type u}
{S : Type v}
{A : Type w}
{B : Type u₁}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R S]
[algebra S A]
[algebra S B] :
(A →ₐ[S] B) → (algebra.comap R S A →ₐ[R] algebra.comap R S B)
R ⟶ S induces S-Alg ⥤ R-Alg
@[instance]
Equations
- rat.algebra_rat = (rat.cast_hom α).to_algebra' rat.algebra_rat._proof_1
structure
subalgebra
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
Type v
- carrier : subsemiring A
- algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ c.carrier
A subalgebra is a subring that includes the range of algebra_map.
@[instance]
def
subalgebra.has_coe
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
has_coe (subalgebra R A) (subsemiring A)
Equations
- subalgebra.has_coe = {coe := λ (S : subalgebra R A), S.carrier}
@[instance]
def
subalgebra.has_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
has_mem A (subalgebra R A)
Equations
- subalgebra.has_mem = {mem := λ (x : A) (S : subalgebra R A), x ∈ ↑S}
theorem
subalgebra.mem_coe
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{x : A}
{s : subalgebra R A} :
@[ext]
theorem
subalgebra.ext
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S T : subalgebra R A} :
theorem
subalgebra.ext_iff
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S T : subalgebra R A} :
theorem
subalgebra.algebra_map_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
(r : R) :
⇑(algebra_map R A) r ∈ S
theorem
subalgebra.srange_le
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
(algebra_map R A).srange ≤ ↑S
theorem
subalgebra.range_subset
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
set.range ⇑(algebra_map R A) ⊆ ↑S
theorem
subalgebra.range_le
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
set.range ⇑(algebra_map R A) ≤ ↑S
theorem
subalgebra.one_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
1 ∈ S
theorem
subalgebra.mul_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{x y : A} :
theorem
subalgebra.smul_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{x : A}
(hx : x ∈ S)
(r : R) :
theorem
subalgebra.pow_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{x : A}
(hx : x ∈ S)
(n : ℕ) :
theorem
subalgebra.zero_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
0 ∈ S
theorem
subalgebra.add_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{x y : A} :
theorem
subalgebra.neg_mem
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A)
{x : A} :
theorem
subalgebra.sub_mem
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A)
{x y : A} :
theorem
subalgebra.nsmul_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{x : A}
(hx : x ∈ S)
(n : ℕ) :
theorem
subalgebra.gsmul_mem
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A)
{x : A}
(hx : x ∈ S)
(n : ℤ) :
theorem
subalgebra.coe_nat_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
(n : ℕ) :
theorem
subalgebra.coe_int_mem
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A)
(n : ℤ) :
theorem
subalgebra.list_prod_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{L : list A} :
theorem
subalgebra.list_sum_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{L : list A} :
theorem
subalgebra.multiset_prod_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(S : subalgebra R A)
{m : multiset A} :
theorem
subalgebra.multiset_sum_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{m : multiset A} :
theorem
subalgebra.prod_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(S : subalgebra R A)
{ι : Type w}
{t : finset ι}
{f : ι → A} :
theorem
subalgebra.sum_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{ι : Type w}
{t : finset ι}
{f : ι → A} :
@[instance]
def
subalgebra.is_add_submonoid
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
- _ = _
@[instance]
def
subalgebra.is_submonoid
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
- _ = _
@[instance]
def
subalgebra.is_subring
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[instance]
def
subalgebra.inhabited
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
@[instance]
def
subalgebra.semiring
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
- subalgebra.semiring R A S = ↑S.to_semiring
@[instance]
def
subalgebra.comm_semiring
(R : Type u)
(A : Type v)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[instance]
def
subalgebra.ring
(R : Type u)
(A : Type v)
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
- subalgebra.ring R A S = subtype.ring
@[instance]
def
subalgebra.comm_ring
(R : Type u)
(A : Type v)
[comm_ring R]
[comm_ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[instance]
def
subalgebra.algebra
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
@[instance]
def
subalgebra.to_algebra
{R : Type u}
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[instance]
def
subalgebra.nontrivial
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
[nontrivial A] :
Equations
- _ = _
def
subalgebra.val
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
Embedding of a subalgebra into the algebra.
@[simp]
theorem
subalgebra.val_apply
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
(x : ↥S) :
def
subalgebra.to_submodule
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
subalgebra R A → submodule R A
Convert a subalgebra to submodule
@[instance]
def
subalgebra.coe_to_submodule
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
has_coe (subalgebra R A) (submodule R A)
Equations
- subalgebra.coe_to_submodule = {coe := subalgebra.to_submodule _inst_3}
@[instance]
def
subalgebra.to_submodule.is_subring
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
- _ = _
@[simp]
theorem
subalgebra.mem_to_submodule
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
{x : A} :
theorem
subalgebra.to_submodule_injective
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S U : subalgebra R A} :
theorem
subalgebra.to_submodule_inj
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S U : subalgebra R A} :
@[instance]
def
subalgebra.partial_order
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
partial_order (subalgebra R A)
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 := _}
def
subalgebra.comap
{R : Type u}
{S : Type v}
{A : Type w}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A] :
subalgebra S A → subalgebra R (algebra.comap R S A)
Reinterpret an S-subalgebra as an R-subalgebra in comap R S A.
def
subalgebra.under
{R : Type u}
{A : Type v}
[comm_semiring R]
[comm_semiring A]
{i : algebra R A}
(S : subalgebra R A) :
subalgebra ↥S A → subalgebra R 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.
def
subalgebra.map
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
[semiring B]
[algebra R B] :
subalgebra R A → (A →ₐ[R] B) → subalgebra R B
Transport a subalgebra via an algebra homomorphism.
Equations
- S.map f = {carrier := subsemiring.map ↑f ↑S, algebra_map_mem' := _}
def
subalgebra.comap'
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
[semiring B]
[algebra R B] :
subalgebra R B → (A →ₐ[R] B) → subalgebra R A
Preimage of a subalgebra under an algebra homomorphism.
Equations
- S.comap' f = {carrier := subsemiring.comap ↑f ↑S, algebra_map_mem' := _}
theorem
subalgebra.map_le
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
[semiring B]
[algebra R B]
{S : subalgebra R A}
{f : A →ₐ[R] B}
{U : subalgebra R B} :
@[instance]
def
subalgebra.integral_domain
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[integral_domain A]
[algebra R A]
(S : subalgebra R A) :
Equations
def
alg_hom.range
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B] :
(A →ₐ[R] B) → subalgebra R B
Range of an alg_hom as a subalgebra.
def
alg_hom.cod_restrict
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B)
(S : subalgebra R B) :
Restrict the codomain of an algebra homomorphism.
theorem
alg_hom.injective_cod_restrict
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B)
(S : subalgebra R B)
(hf : ∀ (x : A), ⇑f x ∈ S) :
function.injective ⇑(f.cod_restrict S hf) ↔ function.injective ⇑f
algebra_map as an alg_hom.
theorem
algebra.of_id_apply
{R : Type u}
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
⇑(algebra.of_id R A) r = ⇑(algebra_map R A) r
def
algebra.adjoin
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
set A → subalgebra R A
The minimal subalgebra that includes s.
Equations
- algebra.adjoin R s = {carrier := subsemiring.closure (set.range ⇑(algebra_map R A) ∪ s), 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 := _}
@[instance]
def
algebra.complete_lattice
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
complete_lattice (subalgebra R A)
@[instance]
def
algebra.inhabited
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
inhabited (subalgebra R A)
Equations
- algebra.inhabited = {default := ⊥}
theorem
algebra.mem_bot
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{x : A} :
theorem
algebra.mem_top
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{x : A} :
@[simp]
theorem
algebra.eq_top_iff
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S : subalgebra R A} :
theorem
algebra.surjective_algbera_map_iff
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
function.surjective ⇑(algebra_map R A) ↔ ⊤ = ⊥
theorem
algebra.bijective_algbera_map_iff
{R : Type u_1}
{A : Type u_2}
[field R]
[semiring A]
[nontrivial A]
[algebra R A] :
function.bijective ⇑(algebra_map R A) ↔ ⊤ = ⊥
def
algebra.bot_equiv_of_injective
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
function.injective ⇑(algebra_map R A) → (↥⊥ ≃ₐ[R] R)
The bottom subalgebra is isomorphic to the base ring.
Equations
def
algebra.bot_equiv
(F : Type u_1)
(R : Type u_2)
[field F]
[semiring R]
[nontrivial R]
[algebra F R] :
The bottom subalgebra is isomorphic to the field.
Equations
@[instance]
Semiring ⥤ ℕ-Alg
Equations
- algebra_nat R = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := (nat.cast_ring_hom R).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
A subsemiring is a ℕ-subalgebra.
Equations
- subalgebra_of_subsemiring S = {carrier := S, algebra_map_mem' := _}
@[simp]
theorem
mem_subalgebra_of_subsemiring
{R : Type u_1}
[semiring R]
{x : R}
{S : subsemiring R} :
x ∈ subalgebra_of_subsemiring S ↔ x ∈ S
@[simp]
theorem
span_nat_eq
{R : Type u_1}
[semiring R]
(s : add_submonoid R) :
(submodule.span ℕ ↑s).to_add_submonoid = s
@[instance]
Ring ⥤ ℤ-Alg
Equations
- algebra_int R = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := (int.cast_ring_hom R).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
A subring is a ℤ-subalgebra.
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem
mem_subalgebra_of_subring
{R : Type u_1}
[ring R]
{x : R}
{S : set R}
[is_subring S] :
x ∈ subalgebra_of_subring S ↔ x ∈ S
@[simp]
theorem
span_int_eq
{R : Type u_1}
[ring R]
(s : add_subgroup R) :
(submodule.span ℤ ↑s).to_add_subgroup = s
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.
@[instance]
def
pi.algebra
(I : Type u)
(f : I → Type v)
(α : Type u_1)
{r : comm_semiring α}
[s : Π (i : I), semiring (f i)]
[Π (i : I), algebra α (f i)] :
algebra α (Π (i : I), f i)
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' := _}
@[simp]
theorem
pi.algebra_map_apply
(I : Type u)
(f : I → Type v)
(α : Type u_1)
{r : comm_semiring α}
[s : Π (i : I), semiring (f i)]
[Π (i : I), algebra α (f i)]
(a : α)
(i : I) :
⇑(algebra_map α (Π (i : I), f i)) a i = ⇑(algebra_map α (f i)) a
theorem
algebra_compatible_smul
{R : Type u_1}
[comm_semiring R]
(A : Type u_2)
[semiring A]
[algebra R A]
{M : Type u_3}
[add_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(r : R)
(m : M) :
r • m = ⇑(algebra_map R A) r • m
theorem
smul_algebra_smul_comm
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[semiring A]
[algebra R A]
{M : Type u_3}
[add_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
(r : R)
(a : A)
(m : M) :
@[simp]
theorem
map_smul_eq_smul_map
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[semiring A]
[algebra R A]
{M : Type u_3}
[add_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
{N : Type u_4}
[add_comm_monoid N]
[semimodule A N]
[semimodule R N]
[is_scalar_tower R A N]
(f : M →ₗ[A] N)
(r : R)
(m : M) :
@[instance]
def
linear_map.has_coe
{R : Type u_1}
[comm_semiring R]
{A : Type u_2}
[semiring A]
[algebra R A]
{M : Type u_3}
[add_comm_monoid M]
[semimodule A M]
[semimodule R M]
[is_scalar_tower R A M]
{N : Type u_4}
[add_comm_monoid N]
[semimodule A N]
[semimodule R N]
[is_scalar_tower R A N] :
def
semimodule.restrict_scalars'
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(E : Type u_3)
[add_comm_monoid E]
[semimodule S E] :
semimodule R E
When E is a module over a ring S, and S is an algebra over R, then E inherits a
module structure over R, called module.restrict_scalars' R S E.
We do not register this as an instance as S can not be inferred.
Equations
- semimodule.restrict_scalars' R S E = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (c : R) (x : E), ⇑(algebra_map R S) c • x}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[nolint]
When E is a module over a ring S, and S is an algebra over R, then E inherits a
module structure over R, provided as a type synonym module.restrict_scalars R S E := E.
When the R-module structure on E is registered directly (using module.restrict_scalars' for
instance, or for S = ℂ and R = ℝ), theorems on module.restrict_scalars R S E can be directly
applied to E as these types are the same for the kernel.
Equations
- semimodule.restrict_scalars R S E = E
@[instance]
def
semimodule.restrict_scalars.inhabited
(R : Type u_1)
(S : Type u_2)
(E : Type u_3)
[I : inhabited E] :
inhabited (semimodule.restrict_scalars R S E)
Equations
@[instance]
def
semimodule.restrict_scalars.add_comm_monoid
(R : Type u_1)
(S : Type u_2)
(E : Type u_3)
[I : add_comm_monoid E] :
Equations
@[instance]
def
semimodule.restrict_scalars.module_orig
(R : Type u_1)
(S : Type u_2)
[semiring S]
(E : Type u_3)
[add_comm_monoid E]
[I : semimodule S E] :
semimodule S (semimodule.restrict_scalars R S E)
Equations
@[instance]
def
semimodule.restrict_scalars.semimodule
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(E : Type u_3)
[add_comm_monoid E]
[semimodule S E] :
semimodule R (semimodule.restrict_scalars R S E)
Equations
theorem
semimodule.restrict_scalars_smul_def
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(E : Type u_3)
[add_comm_monoid E]
[semimodule S E]
(c : R)
(x : semimodule.restrict_scalars R S E) :
c • x = ⇑(algebra_map R S) c • x
def
algebra.restrict_scalars_equiv
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S] :
semimodule.restrict_scalars R S S ≃ₗ[R] S
module.restrict_scalars R S S is R-linearly equivalent to the original algebra S.
Unfortunately these structures are not generally definitionally equal:
the R-module structure on S is part of the data of S,
while the R-module structure on module.restrict_scalars R S S
comes from the ring homomorphism R →+* S, which is a separate part of the data of S.
The field algebra.smul_def' gives the equation we need here.
Equations
- algebra.restrict_scalars_equiv R S = {to_fun := λ (s : semimodule.restrict_scalars R S S), s, map_add' := _, map_smul' := _, inv_fun := λ (s : S), s, left_inv := _, right_inv := _}
@[simp]
theorem
algebra.restrict_scalars_equiv_apply
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(s : S) :
⇑(algebra.restrict_scalars_equiv R S) s = s
@[simp]
theorem
algebra.restrict_scalars_equiv_symm_apply
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(s : S) :
⇑((algebra.restrict_scalars_equiv R S).symm) s = s
@[instance]
def
semimodule.restrict_scalars.is_scalar_tower
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E] :
is_scalar_tower R S (semimodule.restrict_scalars R S E)
Equations
- _ = _
def
submodule.restrict_scalars
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E] :
submodule S E → submodule R (semimodule.restrict_scalars R S E)
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.
@[simp]
theorem
submodule.restrict_scalars_carrier
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E]
(V : submodule S E) :
(submodule.restrict_scalars R V).carrier = V.carrier
@[simp]
theorem
submodule.restrict_scalars_mem
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E]
(V : submodule S E)
(e : E) :
e ∈ submodule.restrict_scalars R V ↔ e ∈ V
@[simp]
theorem
submodule.restrict_scalars_bot
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E] :
@[simp]
theorem
submodule.restrict_scalars_top
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E] :
def
linear_map.restrict_scalars
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E]
{F : Type u_4}
[add_comm_monoid F]
[semimodule S F] :
(E →ₗ[S] F) → (semimodule.restrict_scalars R S E →ₗ[R] semimodule.restrict_scalars R S F)
The R-linear map induced by an S-linear map when S is an algebra over R.
@[simp]
theorem
linear_map.coe_restrict_scalars_eq_coe
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E]
{F : Type u_4}
[add_comm_monoid F]
[semimodule S F]
(f : E →ₗ[S] F) :
⇑(linear_map.restrict_scalars R f) = ⇑f
@[simp]
theorem
restrict_scalars_ker
(R : Type u_1)
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{E : Type u_3}
[add_comm_monoid E]
[semimodule S E]
{F : Type u_4}
[add_comm_monoid F]
[semimodule S F]
(f : E →ₗ[S] F) :
@[instance]
def
semimodule.restrict_scalars.add_comm_group
(R : Type u_1)
(S : Type u_2)
(E : Type u_3)
[I : add_comm_group E] :
Equations
def
subspace.restrict_scalars
(𝕜 : Type u_1)
[field 𝕜]
(𝕜' : Type u_2)
[field 𝕜']
[algebra 𝕜 𝕜']
(W : Type u_3)
[add_comm_group W]
[vector_space 𝕜' W] :
subspace 𝕜' W → subspace 𝕜 (semimodule.restrict_scalars 𝕜 𝕜' W)
V.restrict_scalars 𝕜 is the 𝕜-subspace of the 𝕜-vector space given by restriction of scalars,
corresponding to V, a 𝕜'-subspace of the original 𝕜'-vector space.
Equations
- subspace.restrict_scalars 𝕜 𝕜' W V = {carrier := (submodule.restrict_scalars 𝕜 V).carrier, zero_mem' := _, add_mem' := _, smul_mem' := _}
When V is an R-module and W is an S-module, where S is an algebra over R, then
the collection of R-linear maps from V to W admits an S-module structure, given by
multiplication in the target
@[instance]
def
linear_map.has_scalar_extend_scalars
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(V : Type u_3)
[add_comm_monoid V]
[semimodule R V]
(W : Type u_4)
[add_comm_monoid W]
[semimodule S W] :
has_scalar S (V →ₗ[R] semimodule.restrict_scalars R S W)
The set of R-linear maps admits an S-action by left multiplication
@[instance]
def
linear_map.module_extend_scalars
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(V : Type u_3)
[add_comm_monoid V]
[semimodule R V]
(W : Type u_4)
[add_comm_monoid W]
[semimodule S W] :
semimodule S (V →ₗ[R] semimodule.restrict_scalars R S W)
The set of R-linear maps is an S-module
Equations
- linear_map.module_extend_scalars R S V W = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := linear_map.has_scalar_extend_scalars R S V W _inst_7, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
def
smul_algebra_right
{R : Type u_1}
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{V : Type u_3}
[add_comm_monoid V]
[semimodule R V]
{W : Type u_4}
[add_comm_monoid W]
[semimodule S W] :
(V →ₗ[R] S) → semimodule.restrict_scalars R S W → (V →ₗ[R] semimodule.restrict_scalars R S W)
When f is a linear map taking values in S, then λb, f b • x is a linear map.
@[simp]
theorem
smul_algebra_right_apply
{R : Type u_1}
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{V : Type u_3}
[add_comm_monoid V]
[semimodule R V]
{W : Type u_4}
[add_comm_monoid W]
[semimodule S W]
(f : V →ₗ[R] S)
(x : semimodule.restrict_scalars R S W)
(c : V) :
⇑(smul_algebra_right f x) c = ⇑f c • x
When V and W are S-modules, for some R-algebra S,
the collection of S-linear maps from V to W forms an R-module.
(But not generally an S-module, because S may be non-commutative.)
def
linear_map_algebra_has_scalar
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(V : Type u_3)
[add_comm_monoid V]
[semimodule S V]
(W : Type u_4)
[add_comm_monoid W]
[semimodule S W] :
has_scalar R (V →ₗ[S] W)
For r : R, and f : V →ₗ[S] W (where S is an R-algebra) we define
(r • f) v = f (r • v).
def
linear_map_algebra_module
(R : Type u_1)
[comm_semiring R]
(S : Type u_2)
[semiring S]
[algebra R S]
(V : Type u_3)
[add_comm_monoid V]
[semimodule S V]
(W : Type u_4)
[add_comm_monoid W]
[semimodule S W] :
semimodule R (V →ₗ[S] W)
The R-module structure on S-linear maps, for S an R-algebra.
Equations
- linear_map_algebra_module R S V W = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := linear_map_algebra_has_scalar R S V W _inst_7, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
linear_map_algebra_module.smul_apply
{R : Type u_1}
[comm_semiring R]
{S : Type u_2}
[semiring S]
[algebra R S]
{V : Type u_3}
[add_comm_monoid V]
[semimodule S V]
{W : Type u_4}
[add_comm_monoid W]
[semimodule S W]
(c : R)
(f : V →ₗ[S] W)
(v : V) :