mathlib documentation

algebra.algebra.basic

Algebra over Commutative Semiring #

In this file we define algebras over commutative (semi)rings, algebra homomorphisms alg_hom, algebra equivalences alg_equiv. We also define usual operations on alg_homs (id, comp).

subalgebras are defined in algebra.algebra.subalgebra.

If S is an R-algebra and A is an S-algebra then algebra.comap.algebra R S A can be used to provide A with a structure of an R-algebra. Other than that, algebra.comap is now deprecated and replaced with is_scalar_tower.

For the category of R-algebras, denoted Algebra R, see the file algebra/category/Algebra/basic.lean.

Notations #

@[nolint, class]
structure algebra (R : Type u) (A : Type v) [comm_semiring R] [semiring A] :
Type (max u v)

Given a commutative (semi)ring R, an R-algebra is a (possibly noncommutative) (semi)ring A endowed with a morphism of rings R →+* A which lands in the center of A.

For convenience, this typeclass extends has_scalar R A where the scalar action must agree with left multiplication by the image of the structure morphism.

Given an algebra R A instance, the structure morphism R →+* A is denoted algebra_map R A.

Instances
def algebra_map (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
R →+* A

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) (h : ∀ (c : R) (x : S), (i c) * x = x * i c) :

Creating an algebra from a morphism to the center of a semiring.

Equations
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
theorem ring_hom.algebra_map_to_algebra {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring S] (i : R →+* S) :
def algebra.of_module' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [module 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 module 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.

See note [reducible non-instances].

Equations
def algebra.of_module {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [module 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 module 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.

See note [reducible non-instances].

Equations
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_module {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
module R A
Equations
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.algebra_map_eq_smul_one' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
(algebra_map R A) = λ (r : 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

mul_comm for algebras when one element is from the base ring.

theorem algebra.left_comm {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (x : A) (r : R) (y : A) :
x * ((algebra_map R A) r) * y = ((algebra_map R A) r) * x * y

mul_left_comm for algebras when one element is from the base ring.

theorem algebra.right_comm {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (x : A) (r : R) (y : A) :
(x * (algebra_map R A) r) * y = (x * y) * (algebra_map R A) r

mul_right_comm for algebras when one element is from the base ring.

@[instance]
def is_scalar_tower.right {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] :
@[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

This is just a special case of the global mul_smul_comm lemma that requires less typeclass search (and was here first).

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

This is just a special case of the global smul_mul_assoc lemma that requires less typeclass search (and was here first).

@[simp]
theorem algebra.bit0_smul_one {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit0 r 1 = bit0 (r 1)
theorem algebra.bit0_smul_one' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit0 r 1 = r 2
@[simp]
theorem algebra.bit0_smul_bit0 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit0 r bit0 a = r bit0 (bit0 a)
@[simp]
theorem algebra.bit0_smul_bit1 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit0 r bit1 a = r bit0 (bit1 a)
@[simp]
theorem algebra.bit1_smul_one {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit1 r 1 = bit1 (r 1)
theorem algebra.bit1_smul_one' {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit1 r 1 = r 2 + 1
@[simp]
theorem algebra.bit1_smul_bit0 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit1 r bit0 a = r bit0 (bit0 a) + bit0 a
@[simp]
theorem algebra.bit1_smul_bit1 {R : Type u} {A : Type w} [comm_semiring R] [semiring A] [algebra R A] {r : R} {a : A} :
bit1 r bit1 a = r bit0 (bit1 a) + bit1 a
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
@[simp]
theorem algebra.linear_map_apply (R : Type u) (A : Type w) [comm_semiring R] [semiring A] [algebra R A] (r : R) :
@[instance]
def algebra.id (R : Type u) [comm_semiring R] :
Equations
@[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.prod.algebra (R : Type u) (A : Type w) (B : Type u_1) [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :
algebra R (A × B)
Equations
@[simp]
theorem algebra.algebra_map_prod_apply {R : Type u} {A : Type w} {B : Type u_1} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (r : R) :
(algebra_map R (A × B)) r = ((algebra_map R A) r, (algebra_map R B) r)
@[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. This builds upon subsemiring.module.

Equations
@[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. This builds upon subring.module.

Equations
theorem algebra.algebra_map_of_subring {R : Type u_1} [comm_ring R] (S : subring R) :
theorem algebra.algebra_map_of_subring_apply {R : Type u_1} [comm_ring R] (S : subring R) (x : S) :
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
theorem algebra.is_subring_algebra_map_apply {R : Type u_1} [comm_ring R] (S : set R) [is_subring S] (x : S) :
theorem algebra.set_range_subset {R : Type u_1} [comm_ring R] {T₁ T₂ : set R} [is_subring T₁] (hyp : T₁ T₂) :
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
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

If algebra_map R A is injective and A has no zero divisors, R-multiples in A are zero only if one of the factors is zero.

Cannot be an instance because there is no injective (algebra_map R A) typeclass.

@[instance]
def algebra.no_zero_smul_divisors {R : Type u} {A : Type w} [field R] [semiring A] [algebra R A] [nontrivial A] [no_zero_divisors A] :
@[instance]
def opposite.algebra {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
Equations
@[simp]
theorem opposite.algebra_map_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (c : R) :
@[instance]
def module.endomorphism_algebra (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] :
algebra R (M →ₗ[R] M)
Equations
theorem module.algebra_map_End_eq_smul_id (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) :
@[simp]
theorem module.algebra_map_End_apply (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] (a : R) (m : M) :
((algebra_map R (module.End R M)) a) m = a m
@[simp]
theorem module.ker_algebra_map_End (K : Type u) (V : Type v) [field K] [add_comm_group V] [module K V] (a : K) (ha : a 0) :
@[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
@[simp]
theorem matrix.algebra_map_eq_smul (n : Type u) {R : Type v} [decidable_eq n] [fintype n] [comm_semiring R] (r : R) :
(algebra_map R (matrix n n R)) r = r 1
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] (self : A →ₐ[R] B) :
A →+* 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)

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] :
Equations
@[simp]
theorem alg_hom.to_fun_eq_coe {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) :
@[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
@[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
@[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
@[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.to_ring_hom_eq_coe {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) :
@[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] :
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] :
theorem alg_hom.congr_fun {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.congr_arg {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} (h : x = y) :
φ x = φ y
@[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.mk_coe {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} (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.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) :
@[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)
theorem alg_hom.map_finsupp_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} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) :
φ (f.sum g) = f.sum (λ (i : ι) (a : α), φ (g i a))
@[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.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 : ∀ (c : R) (x : A), f (c x) = c f x) :

If a ring_hom is R-linear, then it is an alg_hom.

Equations
@[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 : ∀ (c : R) (x : A), f (c x) = c f 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
@[simp]
theorem alg_hom.coe_id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem alg_hom.id_to_ring_hom (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
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
@[simp]
theorem alg_hom.coe_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) :
(φ₁.comp φ₂) = φ₁ φ₂
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)
theorem alg_hom.comp_to_ring_hom {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) :
(φ₁.comp φ₂) = (φ₁.comp φ₂)
@[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
@[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) :
theorem alg_hom.to_linear_map_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.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) :
@[simp]
theorem alg_hom.to_linear_map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
def alg_hom.of_linear_map {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) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = (f x) * f y) :

Promote a linear_map to an alg_hom by supplying proofs about the behavior on 1 and *.

Equations
@[simp]
theorem alg_hom.of_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] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = (f x) * f y) (ᾰ : A) :
(alg_hom.of_linear_map f map_one map_mul) = f ᾰ
@[simp]
theorem alg_hom.of_linear_map_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) (map_one : (φ.to_linear_map) 1 = 1) (map_mul : ∀ (x y : A), (φ.to_linear_map) (x * y) = ((φ.to_linear_map) x) * (φ.to_linear_map) y) :
alg_hom.of_linear_map φ.to_linear_map map_one map_mul = φ
@[simp]
theorem alg_hom.to_linear_map_of_linear_map {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) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = (f x) * f y) :
(alg_hom.of_linear_map f map_one map_mul).to_linear_map = f
@[simp]
theorem alg_hom.of_linear_map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (map_one : linear_map.id 1 = 1) (map_mul : ∀ (x y : A), linear_map.id (x * y) = (linear_map.id x) * linear_map.id y) :
theorem alg_hom.map_list_prod {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) (s : list A) :
def alg_hom.fst {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
A × B →ₐ[R] A

First projection as alg_hom.

Equations
def alg_hom.snd {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
A × B →ₐ[R] B

Second projection as alg_hom.

Equations
theorem alg_hom.map_multiset_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) (s : multiset A) :
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)
theorem alg_hom.map_finsupp_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} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) :
φ (f.prod g) = f.prod (λ (i : ι) (a : α), φ (g i a))
@[simp]
theorem alg_hom.map_neg {R : Type u} {A : Type v} {B : Type w} [comm_semiring 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_semiring 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_int_cast {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [ring A] [ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (n : ) :
φ n = n
@[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 = 0x = 0
@[simp]
theorem rat.smul_one_eq_coe {A : Type u_1} [division_ring A] [algebra A] (m : ) :
m 1 = m
@[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] (self : 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] (self : 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] (self : A ≃ₐ[R] B) :
A ≃+* 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)

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] (self : 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₂] :
Equations
@[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.congr_arg {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₂} {x x' : A₁} :
x = x'f x = f x'
theorem alg_equiv.congr_fun {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 : f = g) (x : A₁) :
f x = g x
theorem alg_equiv.ext_iff {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₂} :
f = g ∀ (x : A₁), f x = g x
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
@[simp]
theorem alg_equiv.coe_mk {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} :
{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} = to_fun
@[simp]
theorem alg_equiv.mk_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' : A₂ → A₁) (h₁ : function.left_inverse e' e) (h₂ : function.right_inverse e' e) (h₃ : ∀ (x y : A₁), e (x * y) = (e x) * e y) (h₄ : ∀ (x y : A₁), e (x + y) = e x + e y) (h₅ : ∀ (r : R), e ((algebra_map R A₁) r) = (algebra_map R A₂) r) :
{to_fun := e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅} = e
@[simp]
theorem alg_equiv.to_fun_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₂) :
@[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₂) :
@[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₂] :
@[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
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)
theorem alg_equiv.map_finsupp_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} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A₁) :
e (f.sum g) = f.sum (λ (i : ι) (b : α), e (g i b))
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
@[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
@[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₂) :
@[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.coe_alg_hom_injective {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.coe_ring_hom_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₂) :

The two paths coercion can take to a ring_hom are equivalent

@[simp]
theorem alg_equiv.map_pow {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₁) (n : ) :
e (x ^ n) = e x ^ n
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.has_one {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
has_one (A₁ ≃ₐ[R] A₁)
Equations
@[instance]
def alg_equiv.inhabited {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
inhabited (A₁ ≃ₐ[R] A₁)
Equations
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
@[simp]
theorem alg_equiv.refl_to_alg_hom {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[simp]
theorem alg_equiv.coe_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra 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
def alg_equiv.simps.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₂) :
A₂ → A₁

See Note [custom simps projection]

Equations
@[simp]
theorem alg_equiv.inv_fun_eq_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_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
theorem alg_equiv.symm_bijective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :
@[simp]
theorem alg_equiv.mk_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₂) (f : A₂ → A₁) (h₁ : function.left_inverse e f) (h₂ : function.right_inverse e f) (h₃ : ∀ (x y : A₂), f (x * y) = (f x) * f y) (h₄ : ∀ (x y : A₂), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f ((algebra_map R A₂) r) = (algebra_map R A₁) r) :
{to_fun := f, inv_fun := e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅} = e.symm
@[simp]
theorem alg_equiv.symm_mk {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (f : A₁ → A₂) (f' : A₂ → A₁) (h₁ : function.left_inverse f' f) (h₂ : function.right_inverse f' f) (h₃ : ∀ (x y : A₁), f (x * y) = (f x) * f y) (h₄ : ∀ (x y : A₁), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f ((algebra_map R A₁) r) = (algebra_map R A₂) r) :
{to_fun := f, inv_fun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅}.symm = {to_fun := f', inv_fun := f, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
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
@[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.coe_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₃) :
(e₁.trans e₂) = e₂ e₁
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₂) :
@[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₂) :
theorem alg_equiv.left_inverse_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₂) :
theorem alg_equiv.right_inverse_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₂) :
def alg_equiv.arrow_congr {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {A₁' : Type u_1} {A₂' : Type u_2} [semiring A₁'] [semiring A₂'] [algebra R A₁'] [algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :
(A₁ →ₐ[R] A₂) (A₁' →ₐ[R] A₂')

If A₁ is equivalent to A₁' and A₂ is equivalent to A₂', then the type of maps A₁ →ₐ[R] A₂ is equivalent to the type of maps A₁' →ₐ[R] A₂'.

Equations
theorem alg_equiv.arrow_congr_comp {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₃] {A₁' : Type u_1} {A₂' : Type u_2} {A₃' : Type u_3} [semiring A₁'] [semiring A₂'] [semiring A₃'] [algebra R A₁'] [algebra R A₂'] [algebra R A₃'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') (e₃ : A₃ ≃ₐ[R] A₃') (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₃) :
(e₁.arrow_congr e₃) (g.comp f) = ((e₂.arrow_congr e₃) g).comp ((e₁.arrow_congr e₂) f)
@[simp]
theorem alg_equiv.arrow_congr_refl {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :
@[simp]
theorem alg_equiv.arrow_congr_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₃] {A₁' : Type u_1} {A₂' : Type u_2} {A₃' : Type u_3} [semiring A₁'] [semiring A₂'] [semiring A₃'] [algebra R A₁'] [algebra R A₂'] [algebra R A₃'] (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂') (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃') :
(e₁.trans e₂).arrow_congr (e₁'.trans e₂') = (e₁.arrow_congr e₁').trans (e₂.arrow_congr e₂')
@[simp]
theorem alg_equiv.arrow_congr_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] {A₁' : Type u_1} {A₂' : Type u_2} [semiring A₁'] [semiring A₂'] [algebra R A₁'] [algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :
(e₁.arrow_congr e₂).symm = e₁.symm.arrow_congr e₂.symm
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
theorem alg_equiv.coe_alg_hom_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₁) :
(alg_equiv.of_alg_hom f g h₁ h₂) = f
@[simp]
theorem alg_equiv.of_alg_hom_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₂] (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₁) :
alg_equiv.of_alg_hom f g h₁ h₂ = f
theorem alg_equiv.of_alg_hom_symm {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₁) :
(alg_equiv.of_alg_hom f g h₁ h₂).symm = alg_equiv.of_alg_hom g f h₂ h₁
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
@[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₂) (ᾰ : A₁) :
(e.to_linear_equiv) ᾰ = e ᾰ
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
@[simp]
theorem alg_equiv.to_linear_equiv_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[simp]
theorem alg_equiv.to_linear_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₂) :
@[simp]
theorem alg_equiv.to_linear_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₃) :
theorem alg_equiv.to_linear_equiv_injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :
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
@[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₂) :
@[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₂) :
@[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₁) :
theorem alg_equiv.to_linear_map_injective {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] :
@[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₃) :
@[simp]
theorem alg_equiv.of_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₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), l (x * y) = (l x) * l y) (commutes : ∀ (r : R), l ((algebra_map R A₁) r) = (algebra_map R A₂) r) (ᾰ : A₁) :
(alg_equiv.of_linear_equiv l map_mul commutes) = l ᾰ
def alg_equiv.of_linear_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), l (x * y) = (l x) * l y) (commutes : ∀ (r : R), l ((algebra_map R A₁) r) = (algebra_map R A₂) r) :
A₁ ≃ₐ[R] A₂

Upgrade a linear equivalence to an algebra equivalence, given that it distributes over multiplication and action of scalars.

Equations
@[simp]
theorem alg_equiv.of_linear_equiv_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), l (x * y) = (l x) * l y) (commutes : ∀ (r : R), l ((algebra_map R A₁) r) = (algebra_map R A₂) r) :
@[simp]
theorem alg_equiv.of_linear_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₂) (map_mul : ∀ (x y : A₁), (e.to_linear_equiv) (x * y) = ((e.to_linear_equiv) x) * (e.to_linear_equiv) y) (commutes : ∀ (r : R), (e.to_linear_equiv) ((algebra_map R A₁) r) = (algebra_map R A₂) r) :
@[simp]
theorem alg_equiv.to_linear_equiv_of_linear_equiv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_mul : ∀ (x y : A₁), l (x * y) = (l x) * l y) (commutes : ∀ (r : R), l ((algebra_map R A₁) r) = (algebra_map R A₂) r) :
@[instance]
def alg_equiv.aut {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
group (A₁ ≃ₐ[R] A₁)
Equations
@[simp]
theorem alg_equiv.mul_apply {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) :
(e₁ * e₂) x = e₁ (e₂ x)
def alg_equiv.aut_congr {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) :
(A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂

An algebra isomorphism induces a group isomorphism between automorphism groups

Equations
@[simp]
theorem alg_equiv.aut_congr_apply {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₁ ≃ₐ[R] A₁) :
(ϕ.aut_congr) ψ = ϕ.symm.trans (ψ.trans ϕ)
@[simp]
theorem alg_equiv.aut_congr_refl {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :
@[simp]
theorem alg_equiv.aut_congr_symm {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [semiring A₁] [semiring A₂] [algebra R A₁] [algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) :
@[simp]
theorem alg_equiv.aut_congr_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₃] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) :
theorem alg_equiv.map_prod {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [comm_semiring A₁] [comm_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)
theorem alg_equiv.map_finsupp_prod {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_semiring R] [comm_semiring A₁] [comm_semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {α : Type u_1} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A₁) :
e (f.prod g) = f.prod (λ (i : ι) (a : α), e (g i a))
@[simp]
theorem alg_equiv.map_neg {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [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} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [ring A₁] [ring 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_inv {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [division_ring A₁] [division_ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁) :
@[simp]
theorem alg_equiv.map_div {R : Type u} {A₁ : Type v} {A₂ : Type w} [comm_ring R] [division_ring A₁] [division_ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x y : A₁) :
e (x / y) = e x / e y

matrix section #

Specialize matrix.one_map and matrix.zero_map to alg_hom and alg_equiv. TODO: there should be a way to avoid restating these for each foo_hom.

@[simp]
theorem matrix.alg_hom_map_one {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {n : Type u_4} [fintype n] [comm_semiring R] [semiring A₁] [algebra R A₁] [semiring A₂] [algebra R A₂] [decidable_eq n] (f : A₁ →ₐ[R] A₂) :
1.map f = 1

A version of matrix.one_map where f is an alg_hom.

@[simp]
theorem matrix.alg_equiv_map_one {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {n : Type u_4} [fintype n] [comm_semiring R] [semiring A₁] [algebra R A₁] [semiring A₂] [algebra R A₂] [decidable_eq n] (f : A₁ ≃ₐ[R] A₂) :
1.map f = 1

A version of matrix.one_map where f is an alg_equiv.

@[simp]
theorem matrix.alg_hom_map_zero {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {n : Type u_4} [fintype n] [comm_semiring R] [semiring A₁] [algebra R A₁] [semiring A₂] [algebra R A₂] (f : A₁ →ₐ[R] A₂) :
0.map f = 0

A version of matrix.zero_map where f is an alg_hom.

@[simp]
theorem matrix.alg_equiv_map_zero {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {n : Type u_4} [fintype n] [comm_semiring R] [semiring A₁] [algebra R A₁] [semiring A₂] [algebra R A₂] (f : A₁ ≃ₐ[R] A₂) :
0.map f = 0

A version of matrix.zero_map where f is an alg_equiv.

@[instance]
def nat_algebra_subsingleton {R : Type u_1} [semiring R] :
def ring_hom.to_nat_alg_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) :

Reinterpret a ring_hom as an -algebra homomorphism.

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

Reinterpret a ring_hom as a -algebra homomorphism.

Equations
@[simp]
theorem ring_hom.map_rat_algebra_map {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →+* S) (r : ) :
def ring_hom.to_rat_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra R] [algebra S] (f : R →+* S) :

Reinterpret a ring_hom as a -algebra homomorphism.

Equations
@[instance]
def rat.algebra_rat {α : Type u_1} [division_ring α] [char_zero α] :
Equations
theorem rat.algebra_rat_subsingleton {α : Type u_1} [semiring α] :
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
theorem algebra.of_id_apply {R : Type u} (A : Type v) [comm_semiring R] [semiring A] [algebra R A] (r : R) :
def algebra.lmul (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

The multiplication in an algebra is a bilinear map.

Equations
def algebra.lmul_left (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (r : A) :

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

Equations
def algebra.lmul_right (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (r : A) :

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

Equations
def algebra.lmul_left_right (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (vw : A × A) :

Simultaneous multiplication on the left and right is a linear map.

Equations
def algebra.lmul' (R : Type u) {A : Type v} [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
theorem algebra.commute_lmul_left_right (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a b : A) :
@[simp]
theorem algebra.lmul_apply {R : Type u} {A : Type v} [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 v} [comm_semiring R] [semiring A] [algebra R A] (p q : A) :
@[simp]
theorem algebra.lmul_right_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (p q : A) :
@[simp]
theorem algebra.lmul_left_right_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (vw : A × A) (p : A) :
(algebra.lmul_left_right R vw) p = ((vw.fst) * p) * vw.snd
@[simp]
theorem algebra.lmul_left_one {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem algebra.lmul_left_mul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a b : A) :
@[simp]
theorem algebra.lmul_right_one {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem algebra.lmul_right_mul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a b : A) :
@[simp]
theorem algebra.lmul_left_zero_eq_zero {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem algebra.lmul_right_zero_eq_zero {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem algebra.lmul_left_eq_zero_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
@[simp]
theorem algebra.lmul_right_eq_zero_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
@[simp]
theorem algebra.pow_lmul_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) (n : ) :
@[simp]
theorem algebra.pow_lmul_right {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) (n : ) :
@[simp]
theorem algebra.lmul'_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {x y : A} :
(algebra.lmul' R) (x ⊗ₜ[R] y) = x * y
@[instance]
def algebra.linear_map.module' (R : Type u) [comm_semiring R] (M : Type v) [add_comm_monoid M] [module R M] (S : Type w) [comm_semiring S] [algebra R S] :
module S (M →ₗ[R] S)
Equations
theorem algebra.lmul_left_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x 0) :
theorem algebra.lmul_right_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x 0) :
theorem algebra.lmul_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x 0) :
@[instance]
def algebra_int (R : Type u_1) [ring R] :

Ring ⥤ ℤ-Alg

Equations
@[instance]
def int_algebra_subsingleton {R : Type u_1} [ring R] :

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) {R : Type u_1} (f : I → Type v) {r : comm_semiring R} [s : Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] :
algebra R (Π (i : I), f i)
Equations
@[simp]
theorem pi.algebra_map_apply (I : Type u) {R : Type u_1} (f : I → Type v) {r : comm_semiring R} [s : Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] (a : R) (i : I) :
(algebra_map R (Π (i : I), f i)) a i = (algebra_map R (f i)) a
@[simp]
theorem pi.eval_alg_hom_apply {I : Type u} (R : Type u_1) (f : I → Type v) {r : comm_semiring R} [Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] (i : I) (f_1 : Π (i : I), f i) :
(pi.eval_alg_hom R f i) f_1 = f_1 i
def pi.eval_alg_hom {I : Type u} (R : Type u_1) (f : I → Type v) {r : comm_semiring R} [Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] (i : I) :
(Π (i : I), f i) →ₐ[R] f i

function.eval as an alg_hom. The name matches pi.eval_ring_hom, pi.eval_monoid_hom, etc.

Equations
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] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (m : M) :
r m = (algebra_map R A) r m
@[simp]
theorem algebra_map_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] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (m : M) :
(algebra_map R A) r m = r m
@[instance]
def is_scalar_tower.to_smul_comm_class {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] :
@[instance]
def is_scalar_tower.to_smul_comm_class' {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A 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] [module A M] [module R M] [is_scalar_tower R A M] (r : R) (a : A) (m : M) :
a r m = r a m
@[instance]
def linear_map.coe_is_scalar_tower {R : Type u_1} [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] :
has_coe (M →ₗ[A] N) (M →ₗ[R] N)
Equations
@[simp]
theorem linear_map.coe_restrict_scalars_eq_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] [module A M] [module R M] [is_scalar_tower R A M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
@[simp]
theorem linear_map.coe_coe_is_scalar_tower (R : Type u_1) [comm_semiring R] {A : Type u_2} [semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
def linear_map.lto_fun (R : Type u) (M : Type v) (A : Type w) [comm_semiring R] [add_comm_monoid M] [module R M] [comm_ring A] [algebra R A] :
(M →ₗ[R] A) →ₗ[A] M → A

A-linearly coerce a R-linear map from M to A to a function, given an algebra A over a commutative semiring R and M a module over R.

Equations
@[nolint]
def restrict_scalars (R : Type u_1) (S : Type u_2) (M : Type u_3) :
Type u_3

If we put an R-algebra structure on a semiring S, we get a natural equivalence from the category of S-modules to the category of representations of the algebra S (over R). The type synonym restrict_scalars is essentially this equivalence.

Warning: use this type synonym judiciously! Consider an example where we want to construct an R-linear map from M to S, given:

variables (R S M : Type*)
variables [comm_semiring R] [semiring S] [algebra R S] [add_comm_monoid M] [module S M]

With the assumptions above we can't directly state our map as we have no module R M structure, but restrict_scalars permits it to be written as:

-- an `R`-module structure on `M` is provided by `restrict_scalars` which is compatible
example : restrict_scalars R S M →ₗ[R] S := sorry

However, it is usually better just to add this extra structure as an argument:

-- an `R`-module structure on `M` and proof of its compatibility is provided by the user
example [module R M] [is_scalar_tower R S M] : M →ₗ[R] S := sorry

The advantage of the second approach is that it defers the duty of providing the missing typeclasses [module R M] [is_scalar_tower R S M]. If some concrete M naturally carries these (as is often the case) then we have avoided restrict_scalars entirely. If not, we can pass restrict_scalars R S M later on instead of M.

Note that this means we almost always want to state definitions and lemmas in the language of is_scalar_tower rather than restrict_scalars.

An example of when one might want to use restrict_scalars would be if one has a vector space over a field of characteristic zero and wishes to make use of the -algebra structure.

Equations
@[instance]
def restrict_scalars.inhabited (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : inhabited M] :
Equations
@[instance]
def restrict_scalars.add_comm_monoid (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : add_comm_monoid M] :
Equations
@[instance]
def restrict_scalars.add_comm_group (R : Type u_1) (S : Type u_2) (M : Type u_3) [I : add_comm_group M] :
Equations
@[instance]
def restrict_scalars.module_orig (R : Type u_1) (S : Type u_2) (M : Type u_3)