mathlib documentation

ring_theory.algebra

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 from A to B.
A ≃ₐ[R] B : R-algebra equivalence from A to B.

@[nolint, class]

structure algebra (R : Type u) (A : Type v) [comm_semiring R] [semiring A] :

Type (max u v)

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

def algebra_map (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

Embedding R →+* A given by algebra structure.

Equations

algebra_map R A = algebra.to_ring_hom

def ring_hom.to_algebra' {R : Type u_1} {S : Type u_2} [comm_semiring R] [semiring S] (i : R →+* S) (h : ∀ (c : R) (x : S), (⇑i c) * x = x * ⇑i c) :

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 := {to_fun := i.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := h, smul_def' := _}

def ring_hom.to_algebra {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring S] (i : R →+* S) :

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] (h₁ : ∀ (r : R) (x : A), (r • 1) * x = r • x) (h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x) :

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] (h₁ : ∀ (r : R) (x y : A), (r • x) * y = r • x * y) (h₂ : ∀ (r : R) (x y : A), x * r • y = r • x * y) :

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) (w : ∀ (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] :

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) :

x * s • y = s • x * y

@[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) :

(r • x) * y = r • x * y

def algebra.linear_map (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] :

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' := _}

@[simp]

theorem algebra.linear_map_apply (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] (r : R) :

⇑(algebra.linear_map R A) r = ⇑(algebra_map R A) r

@[instance]

def algebra.id (R : Type u) [comm_semiring R] :

Equations

algebra.id R = (ring_hom.id R).to_algebra

@[simp]

theorem algebra.id.map_eq_self {R : Type u} [comm_semiring R] (x : R) :

⇑(algebra_map R R) x = x

@[simp]

theorem algebra.id.smul_eq_mul {R : Type u} [comm_semiring R] (x y : R) :

x • y = x * y

@[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.

Equations

algebra.of_subsemiring S = {to_has_scalar := {smul := λ (s : ↥S) (x : A), ↑s • x}, to_ring_hom := {to_fun := ((algebra_map R A).comp S.subtype).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

@[instance]

def algebra.of_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : subring R) :

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 S.subtype).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

theorem algebra.algebra_map_of_subring {R : Type u_1} [comm_ring R] (S : subring R) :

algebra_map ↥S R = S.subtype

theorem algebra.coe_algebra_map_of_subring {R : Type u_1} [comm_ring R] (S : subring R) :

⇑(algebra_map ↥S R) = subtype.val

theorem algebra.algebra_map_of_subring_apply {R : Type u_1} [comm_ring R] (S : subring R) (x : ↥S) :

⇑(algebra_map ↥S R) x = ↑x

@[instance]

def algebra.of_is_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 set that is closed under the ring operations.

Equations

algebra.of_is_subring S = algebra.of_subring S.to_subring

theorem algebra.is_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.is_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.is_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

theorem algebra.set_range_subset {R : Type u_1} [comm_ring R] {T₁ T₂ : set R} [is_subring T₁] (hyp : T₁ ⊆ T₂) :

set.range ⇑(algebra_map ↥T₁ R) ⊆ T₂

def algebra.lmul (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] :

A →ₗ[R] A →ₗ[R] A

The multiplication in an algebra is a bilinear map.

Equations

algebra.lmul R A = linear_map.mk₂ R has_mul.mul _ _ _ _

def algebra.lmul_left (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] (r : A) :

The multiplication on the left in an algebra is a linear map.

Equations

algebra.lmul_left R A r = ⇑(algebra.lmul R A) r

def algebra.lmul_right (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] (r : A) :

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] (vw : A × 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)

def algebra.lmul' (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] :

A ⊗ A →ₗ[R] A

The multiplication map on an algebra, as an R-linear map from A ⊗[R] A to A.

Equations

algebra.lmul' R A = tensor_product.lift (algebra.lmul R A)

@[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) :

⇑(algebra.lmul_left_right R A vw) p = ((vw.fst) * p) * vw.snd

@[simp]

theorem algebra.lmul'_apply {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {x y : A} :

⇑(algebra.lmul' R A) (x ⊗ₜ[R] y) = x * y

def algebra.algebra_map_submonoid {R : Type u} [comm_semiring R] (S : Type u_1) [semiring S] [algebra R S] (M : submonoid R) :

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

theorem algebra.mem_algebra_map_submonoid_of_mem {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] [algebra R S] {M : submonoid R} (x : ↥M) :

⇑(algebra_map R S) ↑x ∈ algebra.algebra_map_submonoid S M

@[instance]

def algebra.linear_map.semimodule' (R : Type u) [comm_semiring R] (M : Type v) [add_comm_monoid M] [semimodule R M] (S : Type w) [comm_semiring S] [algebra R S] :

semimodule S (M →ₗ[R] S)

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 := _}

def algebra.semiring_to_ring (R : Type u) {A : Type w} [comm_ring R] [semiring A] [algebra R A] :

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), 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 := _}

theorem algebra.mul_sub_algebra_map_commutes {R : Type u} {A : Type w} [comm_ring R] [ring A] [algebra R A] (x : A) (r : R) :

x * (x - ⇑(algebra_map R A) r) = (x - ⇑(algebra_map R A) r) * x

theorem algebra.mul_sub_algebra_map_pow_commutes {R : Type u} {A : Type w} [comm_ring R] [ring A] [algebra R A] (x : A) (r : R) (n : ℕ) :

x * (x - ⇑(algebra_map R A) r) ^ n = ((x - ⇑(algebra_map R A) r) ^ n) * x

@[instance]

def module.endomorphism_algebra (R : Type u) (M : Type v) [comm_ring R] [add_comm_group M] [module R M] :

algebra R (M →ₗ[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' := _}

theorem module.algebra_map_End_eq_smul_id (R : Type u) (M : Type v) [comm_ring R] [add_comm_group M] [module R M] (a : R) :

⇑(algebra_map R (module.End R M)) a = a • linear_map.id

theorem module.algebra_map_End_apply (R : Type u) (M : Type v) [comm_ring R] [add_comm_group M] [module R M] (a : R) (m : M) :

⇑(⇑(algebra_map R (module.End R M)) a) m = a • m

theorem module.ker_algebra_map_End (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] (a : K) (ha : a ≠ 0) :

linear_map.ker (⇑(algebra_map K (module.End K V)) a) = ⊥

@[instance]

def matrix_algebra (n : Type u) (R : Type v) [decidable_eq n] [fintype n] [comm_semiring R] :

algebra R (matrix n n R)

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' := _}

def alg_hom.to_ring_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (s : A →ₐ[R] B) :

Reinterpret an alg_hom as a ring_hom

@[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)

Equations

alg_hom.has_coe_to_fun = {F := λ (f : A →ₐ[R] B), A → B, coe := λ (f : A →ₐ[R] B), f.to_fun}

@[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] :

has_coe (A →ₐ[R] B) (A →+* B)

Equations

alg_hom.coe_ring_hom = {coe := alg_hom.to_ring_hom _inst_7}

@[instance]

def alg_hom.coe_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

has_coe (A →ₐ[R] B) (A →* B)

Equations

alg_hom.coe_monoid_hom = {coe := λ (f : A →ₐ[R] B), ↑↑f}

@[instance]

def alg_hom.coe_add_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

has_coe (A →ₐ[R] B) (A →+ B)

Equations

alg_hom.coe_add_monoid_hom = {coe := λ (f : A →ₐ[R] B), ↑↑f}

@[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) :

⇑{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅} = f

@[simp]

theorem alg_hom.coe_to_ring_hom {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) :

theorem alg_hom.coe_to_monoid_hom {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) :

theorem alg_hom.coe_to_add_monoid_hom {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) :

theorem alg_hom.coe_fn_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⦄ (H : ⇑φ₁ = ⇑φ₂) :

φ₁ = φ₂

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] :

function.injective coe

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] :

function.injective coe

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] :

function.injective coe

@[ext]

theorem alg_hom.ext {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} (H : ∀ (x : A), ⇑φ₁ x = ⇑φ₂ x) :

φ₁ = φ₂

theorem alg_hom.ext_iff {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} :

φ₁ = φ₂ ↔ ∀ (x : A), ⇑φ₁ x = ⇑φ₂ x

@[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

@[simp]

theorem alg_hom.map_add {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 s : A) :

⇑φ (r + s) = ⇑φ r + ⇑φ s

@[simp]

theorem alg_hom.map_zero {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) :

⇑φ 0 = 0

@[simp]

theorem alg_hom.map_mul {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) (x y : A) :

⇑φ (x * y) = (⇑φ x) * ⇑φ y

@[simp]

theorem alg_hom.map_one {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) :

⇑φ 1 = 1

@[simp]

theorem alg_hom.map_smul {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) (x : A) :

⇑φ (r • x) = r • ⇑φ x

@[simp]

theorem alg_hom.map_pow {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) (x : A) (n : ℕ) :

⇑φ (x ^ n) = ⇑φ x ^ n

theorem alg_hom.map_sum {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) {ι : Type u_1} (f : ι → A) (s : finset ι) :

⇑φ (∑ (x : ι) in s, f x) = ∑ (x : ι) in s, ⇑φ (f x)

@[simp]

theorem alg_hom.map_nat_cast {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) (n : ℕ) :

⇑φ ↑n = ↑n

@[simp]

theorem alg_hom.map_bit0 {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) (x : A) :

⇑φ (bit0 x) = bit0 (⇑φ x)

@[simp]

theorem alg_hom.map_bit1 {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) (x : A) :

⇑φ (bit1 x) = bit1 (⇑φ x)

def alg_hom.id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

Identity map as an alg_hom.

Equations

alg_hom.id R A = {to_fun := (ring_hom.id A).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[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] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :

Composition of algebra homeomorphisms.

Equations

φ₁.comp φ₂ = {to_fun := (φ₁.to_ring_hom.comp ↑φ₂).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[simp]

theorem alg_hom.comp_apply {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] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) :

⇑(φ₁.comp φ₂) p = ⇑φ₁ (⇑φ₂ p)

@[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 φ = φ

theorem alg_hom.comp_assoc {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [semiring D] [algebra R A] [algebra R B] [algebra R C] [algebra R D] (φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B) :

(φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)

def alg_hom.to_linear_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) :

R-Alg ⥤ R-Mod

Equations

φ.to_linear_map = {to_fun := ⇑φ, map_add' := _, map_smul' := _}

@[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} (H : φ₁.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 ι) :

⇑φ (∏ (x : ι) in s, f x) = ∏ (x : ι) in s, ⇑φ (f x)

@[simp]

theorem alg_hom.map_neg {R : Type u} {A : Type v} {B : Type w} [comm_ring R] [ring A] [ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :

⇑φ (-x) = -⇑φ x

@[simp]

theorem alg_hom.map_sub {R : Type u} {A : Type v} {B : Type w} [comm_ring R] [ring A] [ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x y : A) :

⇑φ (x - y) = ⇑φ x - ⇑φ y

@[simp]

theorem alg_hom.map_inv {R : Type u} {A : Type v} {B : Type w} [comm_ring R] [division_ring A] [division_ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :

⇑φ x⁻¹ = (⇑φ x)⁻¹

@[simp]

theorem alg_hom.map_div {R : Type u} {A : Type v} {B : Type w} [comm_ring R] [division_ring A] [division_ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x y : A) :

⇑φ (x / y) = ⇑φ x / ⇑φ y

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) :

function.injective ⇑f ↔ ∀ (x : A), ⇑f x = 0 → x = 0

@[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] (s : A ≃ₐ[R] B) :

A ≃+ 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] (s : A ≃ₐ[R] B) :

A ≃ 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] (s : A ≃ₐ[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_mul_equiv {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (s : A ≃ₐ[R] B) :

A ≃* 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}

@[ext]

theorem alg_equiv.ext {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {f g : A₁ ≃ₐ[R] A₂} (h : ∀ (a : A₁), ⇑f a = ⇑g a) :

f = g

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₂] :

has_coe (A₁ ≃ₐ[R] A₂) (A₁ ≃+* 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₁} :

⇑{to_fun := to_fun, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul, map_add' := map_add, commutes' := commutes} a = to_fun a

@[simp]

theorem alg_equiv.to_fun_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₂} {a : A₁} :

e.to_fun a = ⇑e a

@[simp]

theorem alg_equiv.coe_ring_equiv {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.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.map_add {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 y : A₁) :

⇑e (x + y) = ⇑e x + ⇑e y

@[simp]

theorem alg_equiv.map_zero {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₂) :

⇑e 0 = 0

@[simp]

theorem alg_equiv.map_mul {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 y : A₁) :

⇑e (x * y) = (⇑e x) * ⇑e y

@[simp]

theorem alg_equiv.map_one {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₂) :

⇑e 1 = 1

@[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

@[simp]

theorem alg_equiv.map_neg {R : Type u} [comm_semiring R] {A₁ : Type v} {A₂ : Type w} [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :

⇑e (-x) = -⇑e x

@[simp]

theorem alg_equiv.map_sub {R : Type u} [comm_semiring R] {A₁ : Type v} {A₂ : Type w} [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x y : A₁) :

⇑e (x - y) = ⇑e x - ⇑e y

theorem alg_equiv.map_sum {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₂) {ι : Type u_1} (f : ι → A₁) (s : finset ι) :

⇑e (∑ (x : ι) in s, f x) = ∑ (x : ι) in s, ⇑e (f x)

def alg_equiv.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₂] (e : A₁ ≃ₐ[R] A₂) :

A₁ →ₐ[R] A₂

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

e.to_alg_hom = {to_fun := e.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[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₂] :

has_coe (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂)

Equations

alg_equiv.has_coe_to_alg_hom = {coe := alg_equiv.to_alg_hom _inst_6}

@[simp]

theorem alg_equiv.to_alg_hom_eq_coe {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₂) :

e.to_alg_hom = ↑e

@[simp]

theorem alg_equiv.coe_alg_hom {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.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₂) :

function.injective ⇑e

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₂) :

function.surjective ⇑e

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₂) :

function.bijective ⇑e

@[instance]

def alg_equiv.has_one {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

has_one (A₁ ≃ₐ[R] A₁)

Equations

alg_equiv.has_one = {one := {to_fun := 1.to_fun, inv_fun := 1.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}}

@[instance]

def alg_equiv.inhabited {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

inhabited (A₁ ≃ₐ[R] A₁)

Equations

alg_equiv.inhabited = {default := 1}

def alg_equiv.refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

A₁ ≃ₐ[R] A₁

Algebra equivalences are reflexive.

Equations

alg_equiv.refl = 1

@[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₂] (e : A₁ ≃ₐ[R] A₂) :

A₂ ≃ₐ[R] A₁

Algebra equivalences are symmetric.

Equations

e.symm = {to_fun := e.to_ring_equiv.symm.to_fun, inv_fun := e.to_ring_equiv.symm.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

@[simp]

theorem alg_equiv.inv_fun_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₂} {a : A₂} :

e.inv_fun a = ⇑(e.symm) a

@[simp]

theorem alg_equiv.symm_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₂} :

e.symm.symm = e

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₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :

A₁ ≃ₐ[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.apply_symm_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 (⇑(e.symm) x) = x

@[simp]

theorem alg_equiv.symm_apply_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.symm) (⇑e x) = x

@[simp]

theorem alg_equiv.trans_apply {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₃] (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁) :

⇑(e₁.trans e₂) x = ⇑e₂ (⇑e₁ x)

@[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₂) :

↑e.comp ↑(e.symm) = alg_hom.id 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₂) :

↑(e.symm).comp ↑e = alg_hom.id 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₁) (h₁ : f.comp g = alg_hom.id R A₂) (h₂ : g.comp f = alg_hom.id R A₁) :

A₁ ≃ₐ[R] A₂

If an algebra morphism has an inverse, it is a algebra isomorphism.

Equations

alg_equiv.of_alg_hom f g h₁ h₂ = {to_fun := f.to_fun, inv_fun := ⇑g, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

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₂) (hf : function.bijective ⇑f) :

A₁ ≃ₐ[R] A₂

Promotes a bijective algebra homomorphism to an algebra equivalence.

Equations

alg_equiv.of_bijective f hf = {to_fun := (ring_equiv.of_bijective ↑f hf).to_fun, inv_fun := (ring_equiv.of_bijective ↑f hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

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₂] (e : A₁ ≃ₐ[R] A₂) :

A₁ ≃ₗ[R] A₂

Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence.

Equations

e.to_linear_equiv = {to_fun := e.to_fun, map_add' := _, map_smul' := _, inv_fun := e.symm.to_fun, left_inv := _, right_inv := _}

@[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

theorem alg_equiv.to_linear_equiv_inj {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {e₁ e₂ : A₁ ≃ₐ[R] A₂} (H : e₁.to_linear_equiv = e₂.to_linear_equiv) :

e₁ = e₂

def alg_equiv.to_linear_map {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₂) :

A₁ →ₗ[R] A₂

Interpret an algebra equivalence as a linear map.

Equations

e.to_linear_map = e.to_alg_hom.to_linear_map

@[simp]

theorem alg_equiv.to_alg_hom_to_linear_map {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₂) :

↑e.to_linear_map = e.to_linear_map

@[simp]

theorem alg_equiv.to_linear_equiv_to_linear_map {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₂) :

e.to_linear_equiv.to_linear_map = e.to_linear_map

@[simp]

theorem alg_equiv.to_linear_map_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_map) x = ⇑e x

theorem alg_equiv.to_linear_map_inj {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {e₁ e₂ : A₁ ≃ₐ[R] A₂} (H : e₁.to_linear_map = e₂.to_linear_map) :

e₁ = e₂

@[simp]

theorem alg_equiv.trans_to_linear_map {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₃] (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) :

(f.trans g).to_linear_map = g.to_linear_map.comp f.to_linear_map

@[nolint]

def algebra.comap (R : Type u) (S : Type v) (A : Type w) :

Type w

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.

Equations

algebra.to_comap R S A = {to_fun := (algebra_map S A).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

Equations

φ.comap = {to_fun := φ.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[instance]

def rat.algebra_rat {α : Type u_1} [division_ring α] [char_zero α] :

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 : set A
one_mem' : 1 ∈ c.carrier
mul_mem' : ∀ {a b : A}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
zero_mem' : 0 ∈ c.carrier
add_mem' : ∀ {a b : A}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ c.carrier

A subalgebra is a sub(semi)ring that includes the range of algebra_map.

def subalgebra.to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : subalgebra R A) :

Reinterpret a subalgebra as a subsemiring.

@[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), {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _}}

@[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} :

x ∈ ↑s ↔ x ∈ s

@[ext]

theorem subalgebra.ext {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) :

S = T

theorem subalgebra.ext_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} :

S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T

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} (hx : x ∈ S) (hy : y ∈ S) :

x * y ∈ S

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) :

r • x ∈ S

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 : ℕ) :

x ^ n ∈ S

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} (hx : x ∈ S) (hy : y ∈ S) :

x + y ∈ S

theorem subalgebra.neg_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) :

-x ∈ S

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} (hx : x ∈ S) (hy : y ∈ S) :

x - y ∈ S

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 : ℕ) :

n •ℕ x ∈ S

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 : ℤ) :

n •ℤ x ∈ S

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} (h : ∀ (x : A), x ∈ L → x ∈ S) :

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} (h : ∀ (x : A), x ∈ L → x ∈ S) :

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} (h : ∀ (x : A), x ∈ m → x ∈ S) :

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} (h : ∀ (x : A), x ∈ m → x ∈ S) :

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} (h : ∀ (x : ι), x ∈ t → f x ∈ S) :

∏ (x : ι) in t, f x ∈ S

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} (h : ∀ (x : ι), x ∈ t → f x ∈ S) :

∑ (x : ι) in t, f x ∈ S

@[instance]

def subalgebra.is_add_submonoid {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

is_add_submonoid ↑S

@[instance]

def subalgebra.is_submonoid {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

is_submonoid ↑S

def subalgebra.to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :

A subalgebra over a ring is also a subring.

Equations

S.to_subring = {carrier := S.to_subsemiring.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, neg_mem' := _}

@[instance]

def subalgebra.is_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :

is_subring ↑S

@[instance]

def subalgebra.inhabited {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

Equations

S.inhabited = {default := 0}

@[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) :

comm_semiring ↥S

Equations

subalgebra.comm_semiring R A S = ↑S.to_comm_semiring

@[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

subalgebra.comm_ring R A S = subtype.comm_ring

@[instance]

def subalgebra.algebra {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

Equations

S.algebra = {to_has_scalar := {smul := λ (c : R) (x : ↥S), ⟨c • x.val, _⟩}, to_ring_hom := {to_fun := ((algebra_map R A).cod_srestrict ↑S _).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

@[instance]

def subalgebra.to_algebra {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [comm_semiring A] [semiring B] [algebra R A] [algebra A B] (A₀ : subalgebra R A) :

algebra ↥A₀ B

Equations

A₀.to_algebra = algebra.of_subsemiring ↑A₀

@[instance]

def subalgebra.nontrivial {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [nontrivial A] :

nontrivial ↥S

def subalgebra.val {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

↥S →ₐ[R] A

Embedding of a subalgebra into the algebra.

Equations

S.val = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[simp]

theorem subalgebra.coe_val {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

⇑(S.val) = coe

theorem subalgebra.val_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (x : ↥S) :

⇑(S.val) x = ↑x

def subalgebra.to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

Convert a subalgebra to submodule

Equations

S.to_submodule = {carrier := ↑S, zero_mem' := _, add_mem' := _, smul_mem' := _}

@[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) :

is_subring ↑↑S

@[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} :

x ∈ ↑S ↔ x ∈ S

theorem subalgebra.to_submodule_injective {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S U : subalgebra R A} (h : ↑S = ↑U) :

S = U

theorem subalgebra.to_submodule_inj {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S U : subalgebra R A} :

↑S = ↑U ↔ S = U

@[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] (iSB : subalgebra S A) :

subalgebra R (algebra.comap R S A)

Reinterpret an S-subalgebra as an R-subalgebra in comap R S A.

Equations

iSB.comap = {carrier := iSB.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

def subalgebra.under {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A] {i : algebra R A} (S : subalgebra R A) (T : subalgebra ↥S 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.

Equations

S.under T = {carrier := T.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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] (S : subalgebra R A) (f : A →ₐ[R] B) :

Transport a subalgebra via an algebra homomorphism.

Equations

S.map f = {carrier := (subsemiring.map ↑f ↑S).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, 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] (S : subalgebra R B) (f : A →ₐ[R] B) :

Preimage of a subalgebra under an algebra homomorphism.

Equations

S.comap' f = {carrier := (subsemiring.comap ↑f ↑S).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

theorem subalgebra.map_mono {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S₁ S₂ : subalgebra R A} {f : A →ₐ[R] B} (a : S₁ ≤ S₂) :

S₁.map f ≤ S₂.map f

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} :

S.map f ≤ U ↔ S ≤ U.comap' f

theorem subalgebra.map_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S₁ S₂ : subalgebra R A} (f : A →ₐ[R] B) (hf : function.injective ⇑f) (ih : S₁.map f = S₂.map f) :

S₁ = S₂

theorem subalgebra.mem_map {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} {y : B} :

y ∈ S.map f ↔ ∃ (x : A) (H : x ∈ S), ⇑f x = y

@[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) :

integral_domain ↥S

Equations

S.integral_domain = subring.domain ↑S

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) :

Range of an alg_hom as a subalgebra.

Equations

φ.range = {carrier := φ.to_ring_hom.srange.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

@[simp]

theorem alg_hom.mem_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) {y : B} :

y ∈ φ.range ↔ ∃ (x : A), ⇑φ x = y

@[simp]

theorem alg_hom.coe_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) :

↑(φ.range) = set.range ⇑φ

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) (hf : ∀ (x : A), ⇑f x ∈ S) :

A →ₐ[R] ↥S

Restrict the codomain of an algebra homomorphism.

Equations

f.cod_restrict S hf = {to_fun := (↑f.cod_srestrict ↑S hf).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

def algebra.of_id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

algebra_map as an alg_hom.

Equations

algebra.of_id R A = {to_fun := (algebra_map R A).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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] (s : set A) :

The minimal subalgebra that includes s.

Equations

algebra.adjoin R s = {carrier := (subsemiring.closure (set.range ⇑(algebra_map R A) ∪ s)).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

theorem algebra.gc {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

galois_connection (algebra.adjoin R) coe

def algebra.gi {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

galois_insertion (algebra.adjoin R) coe

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)

Equations

algebra.complete_lattice = algebra.gi.lift_complete_lattice

@[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} :

x ∈ ⊥ ↔ x ∈ set.range ⇑(algebra_map R A)

theorem algebra.mem_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {x : A} :

@[simp]

theorem algebra.coe_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

@[simp]

theorem algebra.coe_bot {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

↑⊥ = set.range ⇑(algebra_map R A)

theorem algebra.eq_top_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : subalgebra R A} :

S = ⊤ ↔ ∀ (x : A), x ∈ S

@[simp]

theorem algebra.map_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :

⊤.map f = f.range

@[simp]

theorem algebra.map_bot {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :

⊥.map f = ⊥

@[simp]

theorem algebra.comap_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :

⊤.comap' f = ⊤

def algebra.to_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

A →ₐ[R] ↥⊤

alg_hom to ⊤ : subalgebra R A.

Equations

algebra.to_top = {to_fun := λ (x : A), ⟨x, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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] (h : function.injective ⇑(algebra_map R A)) :

↥⊥ ≃ₐ[R] R

The bottom subalgebra is isomorphic to the base ring.

Equations

algebra.bot_equiv_of_injective h = (alg_equiv.of_bijective (algebra.of_id R ↥⊥) _).symm

def algebra.bot_equiv (F : Type u_1) (R : Type u_2) [field F] [semiring R] [nontrivial R] [algebra F R] :

↥⊥ ≃ₐ[F] F

The bottom subalgebra is isomorphic to the field.

Equations

algebra.bot_equiv F R = algebra.bot_equiv_of_injective _

theorem subalgebra.range_val {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

S.val.range = S

def alg_hom_nat {R : Type u} [semiring R] [algebra ℕ R] {S : Type v} [semiring S] [algebra ℕ S] (f : R →+* S) :

R →ₐ[ℕ ] S

Reinterpret a ring_hom as an ℕ-algebra homomorphism.

Equations

alg_hom_nat f = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[instance]

def algebra_nat (R : Type u_1) [semiring R] :

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' := _}

def subalgebra_of_subsemiring {R : Type u_1} [semiring R] (S : subsemiring R) :

subalgebra ℕ R

A subsemiring is a ℕ-subalgebra.

Equations

subalgebra_of_subsemiring S = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, 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

theorem span_nat_eq_add_group_closure {R : Type u_1} [semiring R] (s : set R) :

(submodule.span ℕ s).to_add_submonoid = add_submonoid.closure s

@[simp]

theorem span_nat_eq {R : Type u_1} [semiring R] (s : add_submonoid R) :

(submodule.span ℕ ↑s).to_add_submonoid = s

def alg_hom_int {R : Type u} [comm_ring R] [algebra ℤ R] {S : Type v} [comm_ring S] [algebra ℤ S] (f : R →+* S) :

R →ₐ[ℤ ] S

Reinterpret a ring_hom as a ℤ-algebra homomorphism.

Equations

alg_hom_int f = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[instance]

def algebra_int (R : Type u_1) [ring R] :

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' := _}

def ring_hom.to_int_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R →+* S) :

R →ₐ[ℤ ] S

Promote a ring homomorphisms to a ℤ-algebra homomorphism.

Equations

f.to_int_alg_hom = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

def subalgebra_of_subring {R : Type u_1} [ring R] (S : subring R) :

subalgebra ℤ R

A subring is a ℤ-subalgebra.

Equations

subalgebra_of_subring S = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

def subalgebra_of_is_subring {R : Type u_1} [ring R] (S : set R) [is_subring S] :

subalgebra ℤ R

A subset closed under the ring operations is a ℤ-subalgebra.

Equations

subalgebra_of_is_subring S = subalgebra_of_subring S.to_subring

@[instance]

def int_algebra_subsingleton {S : Type u_2} [ring S] :

subsingleton (algebra ℤ S)

@[instance]

def nat_algebra_subsingleton {S : Type u_2} [semiring S] :

subsingleton (algebra ℕ S)

@[simp]

theorem mem_subalgebra_of_subring {R : Type u_1} [ring R] {x : R} {S : subring R} :

x ∈ subalgebra_of_subring S ↔ x ∈ S

@[simp]

theorem mem_subalgebra_of_is_subring {R : Type u_1} [ring R] {x : R} {S : set R} [is_subring S] :

x ∈ subalgebra_of_is_subring S ↔ x ∈ S

theorem span_int_eq_add_group_closure {R : Type u_1} [ring R] (s : set R) :

(submodule.span ℤ s).to_add_subgroup = add_subgroup.closure 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) :

a • r • m = r • a • 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) :

⇑f (r • m) = r • ⇑f 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] :

has_coe (M →ₗ[A] N) (M →ₗ[R] N)

Equations

linear_map.has_coe = {coe := λ (f : M →ₗ[A] N), {to_fun := f.to_fun, map_add' := _, map_smul' := _}}

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] :

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]

def semimodule.restrict_scalars (R : Type u_1) (S : Type u_2) (E : Type u_3) :

Type u_3

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

semimodule.restrict_scalars.inhabited R S E = I

@[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] :

add_comm_monoid (semimodule.restrict_scalars R S E)

Equations

semimodule.restrict_scalars.add_comm_monoid R S E = I

@[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

semimodule.restrict_scalars.module_orig R S E = I

@[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

semimodule.restrict_scalars.semimodule R S E = semimodule.restrict_scalars' R S E

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)

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] (V : 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.

Equations

submodule.restrict_scalars R V = {carrier := V.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _}

@[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] :

submodule.restrict_scalars R ⊥ = ⊥

@[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] :

submodule.restrict_scalars R ⊤ = ⊤

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] (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.

Equations

linear_map.restrict_scalars R f = {to_fun := f.to_fun, map_add' := _, map_smul' := _}

@[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) :

(linear_map.restrict_scalars R f).ker = submodule.restrict_scalars R f.ker

def linear_map.lto_fun (R : Type u) (M : Type v) (A : Type w) [comm_semiring R] [add_comm_monoid M] [semimodule R M] [comm_ring A] [algebra R A] :

(M →ₗ[R] A) →ₗ[A] M → A

A-linearly coerce a R-linear map from M to R 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' := _}

@[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] :

add_comm_group (semimodule.restrict_scalars R S E)

Equations

semimodule.restrict_scalars.add_comm_group R S E = I

def subspace.restrict_scalars (𝕜 : Type u_1) [field 𝕜] (𝕜' : Type u_2) [field 𝕜'] [algebra 𝕜 𝕜'] (W : Type u_3) [add_comm_group W] [vector_space 𝕜' W] (V : 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

Equations

linear_map.has_scalar_extend_scalars R S V W = {smul := λ (r : S) (f : V →ₗ[R] semimodule.restrict_scalars R S W), {to_fun := λ (v : V), r • ⇑f v, map_add' := _, map_smul' := _}}

@[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] (f : V →ₗ[R] S) (x : 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.

Equations

smul_algebra_right f x = {to_fun := λ (b : V), ⇑f b • x, map_add' := _, map_smul' := _}

@[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).

Equations

linear_map_algebra_has_scalar R S V W = {smul := λ (r : R) (f : V →ₗ[S] W), {to_fun := λ (v : V), ⇑f (⇑(algebra_map R S) r • v), map_add' := _, map_smul' := _}}

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) :

⇑(c • f) v = c • ⇑f v