mathlib documentation

algebra.algebra.basic

Algebras over commutative semirings #

In this file we define algebras over commutative (semi)rings, algebra homomorphisms alg_hom, and algebra equivalences alg_equiv. We also define the 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 #

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

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

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

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

algebra_map R S = i

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

algebra.of_module' h₁ h₂ = {to_has_scalar := smul_with_zero.to_has_scalar (mul_action_with_zero.to_smul_with_zero R A), to_ring_hom := {to_fun := λ (r : R), r • 1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

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

algebra.of_module h₁ h₂ = algebra.of_module' _ _

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

Equations

algebra.to_module = {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.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] :

is_scalar_tower R A 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

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_id {R : Type u} [comm_semiring R] :

algebra_map R R = ring_hom.id R

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

algebra.prod.algebra R A B = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := ((algebra_map R A).prod (algebra_map R B)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

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

algebra.of_subsemiring S = {to_has_scalar := {smul := has_scalar.smul smul_with_zero.to_has_scalar}, 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. This builds upon subring.module.

Equations

algebra.of_subring S = {to_has_scalar := {smul := has_scalar.smul smul_with_zero.to_has_scalar}, to_ring_hom := algebra.to_ring_hom (algebra.of_subsemiring S.to_subsemiring), 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

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

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. See note [reducible non-instances].

Equations

algebra.semiring_to_ring R = {add := add_comm_group.add (module.add_comm_monoid_to_add_comm_group R), add_assoc := _, zero := add_comm_group.zero (module.add_comm_monoid_to_add_comm_group R), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (module.add_comm_monoid_to_add_comm_group R), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (module.add_comm_monoid_to_add_comm_group R), sub := add_comm_group.sub (module.add_comm_monoid_to_add_comm_group R), sub_eq_add_neg := _, gsmul := add_comm_group.gsmul (module.add_comm_monoid_to_add_comm_group R), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semiring.mul infer_instance, mul_assoc := _, one := semiring.one infer_instance, one_mul := _, mul_one := _, npow := semiring.npow infer_instance, npow_zero' := _, npow_succ' := _, 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

theorem no_zero_smul_divisors.of_algebra_map_injective {R : Type u_1} {A : Type u_2} [comm_ring R] [semiring A] [algebra R A] [no_zero_divisors A] (h : function.injective ⇑(algebra_map R A)) :

no_zero_smul_divisors R A

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.

theorem no_zero_smul_divisors.algebra_map_injective (R : Type u_1) (A : Type u_2) [comm_ring R] [ring A] [nontrivial A] [algebra R A] [no_zero_smul_divisors R A] :

function.injective ⇑(algebra_map R A)

theorem no_zero_smul_divisors.iff_algebra_map_injective {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [domain A] [algebra R A] :

no_zero_smul_divisors R A ↔ function.injective ⇑(algebra_map R A)

@[instance]

def no_zero_smul_divisors.algebra.no_zero_smul_divisors {R : Type u_1} {A : Type u_2} [field R] [semiring A] [algebra R A] [nontrivial A] [no_zero_divisors A] :

no_zero_smul_divisors R A

@[instance]

def opposite.algebra {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :

algebra R Aᵒᵖ

Equations

opposite.algebra = {to_has_scalar := {smul := has_scalar.smul (opposite.has_scalar A R)}, to_ring_hom := (algebra_map R A).to_opposite opposite.algebra._proof_1, commutes' := _, smul_def' := _}

@[simp]

theorem opposite.algebra_map_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (c : R) :

⇑(algebra_map R Aᵒᵖ) c = opposite.op (⇑(algebra_map R A) c)

@[instance]

def module.End.algebra (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] :

algebra R (module.End R M)

Equations

module.End.algebra R M = algebra.of_module _ _

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

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

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

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

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

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' : self.to_fun 1 = 1
map_mul' : ∀ (x y : A), self.to_fun (x * y) = (self.to_fun x) * self.to_fun y
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
commutes' : ∀ (r : R), self.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) (λ (_x : A →ₐ[R] B), A → B)

Equations

alg_hom.has_coe_to_fun = {coe := alg_hom.to_fun _inst_7}

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

f.to_fun = ⇑f

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

f.to_ring_hom = ↑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_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_fn

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

⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂

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

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

↑φ.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)

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

alg_hom.mk' f h = {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

⇑(alg_hom.mk' f h) = ⇑f

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.coe_id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

⇑(alg_hom.id R A) = id

@[simp]

theorem alg_hom.id_to_ring_hom (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :

↑(alg_hom.id R A) = ring_hom.id 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

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

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

φ.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_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 alg_hom.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

@[simp]

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

(alg_hom.id R A).to_linear_map = linear_map.id

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

alg_hom.of_linear_map f map_one map_mul = {to_fun := ⇑f, map_one' := map_one, map_mul' := map_mul, map_zero' := _, map_add' := _, commutes' := _}

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

alg_hom.of_linear_map linear_map.id map_one map_mul = alg_hom.id R A

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

⇑φ s.prod = (list.map ⇑φ s).prod

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

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

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

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

theorem alg_hom.algebra_map_eq_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) {y : R} {x : A} (h : ⇑(algebra_map R A) y = x) :

⇑(algebra_map R B) y = ⇑f x

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

⇑φ s.prod = (multiset.map ⇑φ s).prod

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 = 0 → x = 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) :

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 self.inv_fun self.to_fun
right_inv : function.right_inverse self.inv_fun self.to_fun
map_mul' : ∀ (x y : A), self.to_fun (x * y) = (self.to_fun x) * self.to_fun y
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
commutes' : ∀ (r : R), self.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] (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₂] :

has_coe_to_fun (A₁ ≃ₐ[R] A₂) (λ (_x : A₁ ≃ₐ[R] A₂), A₁ → A₂)

Equations

alg_equiv.has_coe_to_fun = {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.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

alg_equiv.has_coe_to_ring_equiv = {coe := alg_equiv.to_ring_equiv _inst_6}

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

e.to_fun = ⇑e

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

⇑(e.to_ring_equiv) = ⇑e

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 coe

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

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

function.injective coe

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

↑↑e = ↑↑e

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

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.refl_to_alg_hom {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] :

↑alg_equiv.refl = alg_hom.id R A₁

@[simp]

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

⇑alg_equiv.refl = id

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

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

alg_equiv.simps.symm_apply e = ⇑(e.symm)

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

e.inv_fun = ⇑(e.symm)

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

function.bijective alg_equiv.symm

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

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.symm_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₂).symm) x = ⇑(e₁.symm) (⇑(e₂.symm) 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₂) :

↑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₁

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

function.left_inverse ⇑(e.symm) ⇑e

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

function.right_inverse ⇑(e.symm) ⇑e

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

e₁.arrow_congr e₂ = {to_fun := λ (f : A₁ →ₐ[R] A₂), (e₂.to_alg_hom.comp f).comp e₁.symm.to_alg_hom, inv_fun := λ (f : A₁' →ₐ[R] A₂'), (e₂.symm.to_alg_hom.comp f).comp e₁.to_alg_hom, left_inv := _, right_inv := _}

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

alg_equiv.refl.arrow_congr alg_equiv.refl = equiv.refl (A₁ →ₐ[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

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

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

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

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

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

@[simp]

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

alg_equiv.refl.to_linear_equiv = linear_equiv.refl 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₂) :

e.to_linear_equiv.symm = e.symm.to_linear_equiv

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

(e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv

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

function.injective alg_equiv.to_linear_equiv

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_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 alg_equiv.to_linear_map

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

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

alg_equiv.of_linear_equiv l map_mul commutes = {to_fun := ⇑l, inv_fun := ⇑(l.symm), left_inv := _, right_inv := _, map_mul' := map_mul, map_add' := _, commutes' := commutes}

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

(alg_equiv.of_linear_equiv l map_mul commutes).symm = alg_equiv.of_linear_equiv l.symm _ _

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

alg_equiv.of_linear_equiv e.to_linear_equiv map_mul commutes = e

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

(alg_equiv.of_linear_equiv l map_mul commutes).to_linear_equiv = l

@[instance]

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

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

Equations

alg_equiv.aut = {mul := λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default 1 (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5, npow_zero' := _, npow_succ' := _, inv := alg_equiv.symm _inst_5, div := div_inv_monoid.div._default (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_8 1 alg_equiv.aut._proof_9 alg_equiv.aut._proof_10 (div_inv_monoid.npow._default 1 (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5) alg_equiv.aut._proof_11 alg_equiv.aut._proof_12 alg_equiv.symm, div_eq_mul_inv := _, gpow := div_inv_monoid.gpow._default (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_14 1 alg_equiv.aut._proof_15 alg_equiv.aut._proof_16 (div_inv_monoid.npow._default 1 (λ (ϕ ψ : A₁ ≃ₐ[R] A₁), ψ.trans ϕ) alg_equiv.aut._proof_4 alg_equiv.aut._proof_5) alg_equiv.aut._proof_17 alg_equiv.aut._proof_18 alg_equiv.symm, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}

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

ϕ.aut_congr = {to_fun := λ (ψ : A₁ ≃ₐ[R] A₁), ϕ.symm.trans (ψ.trans ϕ), inv_fun := λ (ψ : A₂ ≃ₐ[R] A₂), ϕ.trans (ψ.trans ϕ.symm), left_inv := _, right_inv := _, map_mul' := _}

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

alg_equiv.refl.aut_congr = mul_equiv.refl (A₁ ≃ₐ[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₂) :

ϕ.aut_congr.symm = ϕ.symm.aut_congr

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

ϕ.aut_congr.trans ψ.aut_congr = (ϕ.trans ψ).aut_congr

@[instance]

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

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

The tautological action by A₁ ≃ₐ[R] A₁ on A₁.

This generalizes function.End.apply_mul_action.

Equations

alg_equiv.apply_mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (_x : A₁ ≃ₐ[R] A₁) (_y : A₁), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}

@[simp]

theorem alg_equiv.smul_def {R : Type u} {A₁ : Type v} [comm_semiring R] [semiring A₁] [algebra R A₁] (f : A₁ ≃ₐ[R] A₁) (a : A₁) :

f • a = ⇑f a

@[instance]

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

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

@[instance]

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

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

@[instance]

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

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

@[simp]

theorem alg_equiv.algebra_map_eq_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₂) {y : R} {x : A₁} :

⇑(algebra_map R A₂) y = ⇑e x ↔ ⇑(algebra_map R A₁) y = x

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

⇑e x⁻¹ = (⇑e x)⁻¹

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

def mul_semiring_action.to_alg_hom {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] (m : M) :

Each element of the monoid defines a algebra homomorphism.

This is a stronger version of mul_semiring_action.to_ring_hom and distrib_mul_action.to_linear_map.

Equations

mul_semiring_action.to_alg_hom R A m = alg_hom.mk' (mul_semiring_action.to_ring_hom M A m) _

@[simp]

theorem mul_semiring_action.to_alg_hom_apply {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] (m : M) (ᾰ : A) :

⇑(mul_semiring_action.to_alg_hom R A m) ᾰ = m • ᾰ

theorem mul_semiring_action.to_alg_hom_injective {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] [has_faithful_scalar M A] :

function.injective (mul_semiring_action.to_alg_hom R A)

def mul_semiring_action.to_alg_equiv {G : Type u_2} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [group G] [mul_semiring_action G A] [smul_comm_class G R A] (g : G) :

Each element of the group defines a algebra equivalence.

This is a stronger version of mul_semiring_action.to_ring_equiv and distrib_mul_action.to_linear_equiv.

Equations

mul_semiring_action.to_alg_equiv R A g = {to_fun := (mul_semiring_action.to_ring_equiv G A g).to_fun, inv_fun := (mul_semiring_action.to_ring_equiv G A g).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

@[simp]

theorem mul_semiring_action.to_alg_equiv_symm_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [group G] [mul_semiring_action G A] [smul_comm_class G R A] (g : G) (ᾰ : A) :

⇑((mul_semiring_action.to_alg_equiv R A g).symm) ᾰ = (mul_semiring_action.to_ring_equiv G A g).inv_fun ᾰ

@[simp]

theorem mul_semiring_action.to_alg_equiv_apply {G : Type u_2} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [group G] [mul_semiring_action G A] [smul_comm_class G R A] (g : G) (ᾰ : A) :

⇑(mul_semiring_action.to_alg_equiv R A g) ᾰ = (mul_semiring_action.to_ring_equiv G A g).to_fun ᾰ

theorem mul_semiring_action.to_alg_equiv_injective {G : Type u_2} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [group G] [mul_semiring_action G A] [smul_comm_class G R A] [has_faithful_scalar G A] :

function.injective (mul_semiring_action.to_alg_equiv R A)

@[instance]

def algebra_nat {R : Type u_1} [semiring R] :

Semiring ⥤ ℕ-Alg

Equations

algebra_nat = {to_has_scalar := add_monoid.has_scalar_nat (add_comm_monoid.to_add_monoid R), to_ring_hom := nat.cast_ring_hom R (semiring.to_non_assoc_semiring R), commutes' := _, smul_def' := _}

@[instance]

def nat_algebra_subsingleton {R : Type u_1} [semiring R] :

subsingleton (algebra ℕ R)

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

R →ₐ[ℕ ] S

Reinterpret a ring_hom as an ℕ-algebra homomorphism.

Equations

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

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

R →ₐ[ℤ ] S

Reinterpret a ring_hom as a ℤ-algebra homomorphism.

Equations

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

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

⇑f (⇑(algebra_map ℚ R) r) = ⇑(algebra_map ℚ 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) :

R →ₐ[ℚ ] S

Reinterpret a ring_hom as a ℚ-algebra homomorphism.

Equations

f.to_rat_alg_hom = {to_fun := f.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

@[simp]

theorem rat.algebra_map_rat_rat :

algebra_map ℚ ℚ = ring_hom.id ℚ

theorem rat.algebra_rat_subsingleton {α : Type u_1} [semiring α] :

subsingleton (algebra ℚ α)

theorem char_zero.of_algebra {R : Type u_1} (S : Type u_2) [comm_semiring R] [semiring S] [algebra R S] [char_zero S] :

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

@[instance]

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

Ring ⥤ ℤ-Alg

Equations

algebra_int R = {to_has_scalar := sub_neg_monoid.has_scalar_int (add_group.to_sub_neg_monoid R), to_ring_hom := int.cast_ring_hom R _inst_1, commutes' := _, smul_def' := _}

@[instance]

def int_algebra_subsingleton {R : Type u_1} [ring R] :

subsingleton (algebra ℤ 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

pi.algebra I f = {to_has_scalar := pi.has_scalar (λ (i : I), smul_with_zero.to_has_scalar), to_ring_hom := {to_fun := (pi.ring_hom (λ (i : I), algebra_map R (f i))).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

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

pi.eval_alg_hom R f i = {to_fun := λ (f : Π (i : I), f i), f i, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[simp]

theorem pi.const_alg_hom_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring B] [algebra R B] (a : B) (ᾰ : A) :

⇑(pi.const_alg_hom R A B) a ᾰ = function.const A a ᾰ

def pi.const_alg_hom (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring B] [algebra R B] :

B →ₐ[R] A → B

function.const as an alg_hom. The name matches pi.const_ring_hom, pi.const_monoid_hom, etc.

Equations

pi.const_alg_hom R A B = {to_fun := function.const A, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[simp]

theorem pi.const_ring_hom_eq_algebra_map (R : Type u_1) (A : Type u_2) [comm_semiring R] :

pi.const_ring_hom A R = algebra_map R (A → R)

When R is commutative and permits an algebra_map, pi.const_ring_hom is equal to that map.

@[simp]

theorem pi.const_alg_hom_eq_algebra_of_id (R : Type u_1) (A : Type u_2) [comm_semiring R] :

pi.const_alg_hom R A R = algebra.of_id R (A → R)

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

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

smul_comm_class 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] [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

linear_map.coe_is_scalar_tower = {coe := linear_map.restrict_scalars R linear_map.is_scalar_tower.compatible_smul}

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

⇑(linear_map.restrict_scalars R f) = ⇑f

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

linear_map.lto_fun R M A = {to_fun := linear_map.to_fun algebra.to_module, map_add' := _, map_smul' := _}

TODO: The following lemmas no longer involve algebra at all, and could be moved closer to algebra/module/submodule.lean. Currently this is tricky because ker, range, ⊤, and ⊥ are all defined in linear_algebra/basic.lean.

theorem submodule.span_le_restrict_scalars (R : Type u_1) (S : Type u_2) (M : Type u_3) [semiring R] [semiring S] [has_scalar R S] [add_comm_monoid M] [module R M] [module S M] [is_scalar_tower R S M] (X : set M) :

submodule.span R X ≤ submodule.restrict_scalars R (submodule.span S X)

If S is an R-algebra, then the R-module generated by a set X is included in the S-module generated by X.

@[simp]

theorem linear_map.ker_restrict_scalars (R : Type u_1) {S : Type u_2} {M : Type u_3} {N : Type u_4} [semiring R] [semiring S] [has_scalar R S] [add_comm_monoid M] [module R M] [module S M] [is_scalar_tower R S M] [add_comm_monoid N] [module R N] [module S N] [is_scalar_tower R S N] (f : M →ₗ[S] N) :

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

theorem submodule.span_eq_restrict_scalars (R : Type u_1) (A : Type u_2) (M : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] (X : set M) (hsur : function.surjective ⇑(algebra_map R A)) :

submodule.span R X = submodule.restrict_scalars R (submodule.span A X)

If A is an R-algebra such that the induced morhpsim R →+* A is surjective, then the R-module generated by a set X equals the A-module generated by X.

def alg_hom.comp_left {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) (I : Type u_1) :

(I → A) →ₐ[R] I → B

R-algebra homomorphism between the function spaces I → A and I → B, induced by an R-algebra homomorphism f between A and B.

Equations

f.comp_left I = {to_fun := λ (h : I → A), ⇑f ∘ h, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[simp]

theorem alg_hom.comp_left_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) (I : Type u_1) (h : I → A) (ᾰ : I) :

⇑(f.comp_left I) h ᾰ = (⇑f ∘ h) ᾰ