mathlib3 documentation

algebra.algebra.subalgebra.basic

Subalgebras over Commutative Semiring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define subalgebras and the usual operations on them (map, comap).

More lemmas about adjoin can be found in ring_theory.adjoin.

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

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

Instances for subalgebra
source
def subalgebra.to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (self : subalgebra R A) :
subsemiring A

Reinterpret a subalgebra as a subsemiring.

source
@[protected, instance]
def subalgebra.set_like {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
set_like (subalgebra R A) A
Equations
source
@[protected, instance]
def subalgebra.subsemiring_class {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
subsemiring_class (subalgebra R A) A
source
@[simp]
theorem subalgebra.mem_carrier {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : subalgebra R A} {x : A} :
x ∈ s.carrier ↔ x ∈ s
source
@[ext]
theorem subalgebra.ext {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) :
S = T
source
@[simp]
theorem subalgebra.mem_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : subalgebra R A} {x : A} :
x ∈ S.to_subsemiring ↔ x ∈ S
source
@[simp]
theorem subalgebra.coe_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
↑(S.to_subsemiring) = ↑S
source
theorem subalgebra.to_subsemiring_injective {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
function.injective subalgebra.to_subsemiring
source
theorem subalgebra.to_subsemiring_inj {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S U : subalgebra R A} :
S.to_subsemiring = U.to_subsemiring ↔ S = U
source
@[protected]
def subalgebra.copy {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (s : set A) (hs : s = ↑S) :
subalgebra R A

Copy of a subalgebra with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
source
@[simp]
theorem subalgebra.coe_copy {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (s : set A) (hs : s = ↑S) :
↑(S.copy s hs) = s
source
theorem subalgebra.copy_eq {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (s : set A) (hs : s = ↑S) :
S.copy s hs = S
source
theorem subalgebra.algebra_map_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (r : R) :
⇑(algebra_map R A) r ∈ S
source
theorem subalgebra.srange_le {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
(algebra_map R A).srange ≤ S.to_subsemiring
source
theorem subalgebra.range_subset {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
set.range ⇑(algebra_map R A) ⊆ ↑S
source
theorem subalgebra.range_le {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
set.range ⇑(algebra_map R A) ≤ ↑S
source
theorem subalgebra.smul_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) (r : R) :
r • x ∈ S
source
@[protected, instance]
def subalgebra.smul_mem_class {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
smul_mem_class (subalgebra R A) R A
Equations
source
@[protected]
theorem subalgebra.one_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
1 ∈ S
source
@[protected]
theorem subalgebra.mul_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x y : A} (hx : x ∈ S) (hy : y ∈ S) :
x * y ∈ S
source
@[protected]
theorem subalgebra.pow_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) (n : ℕ) :
x ^ n ∈ S
source
@[protected]
theorem subalgebra.zero_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
0 ∈ S
source
@[protected]
theorem subalgebra.add_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x y : A} (hx : x ∈ S) (hy : y ∈ S) :
x + y ∈ S
source
@[protected]
theorem subalgebra.nsmul_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) (n : ℕ) :
n • x ∈ S
source
@[protected]
theorem subalgebra.coe_nat_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (n : ℕ) :
↑n ∈ S
source
@[protected]
theorem subalgebra.list_prod_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {L : list A} (h : ∀ (x : A), x ∈ L → x ∈ S) :
L.prod ∈ S
source
@[protected]
theorem subalgebra.list_sum_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {L : list A} (h : ∀ (x : A), x ∈ L → x ∈ S) :
L.sum ∈ S
source
@[protected]
theorem subalgebra.multiset_sum_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {m : multiset A} (h : ∀ (x : A), x ∈ m → x ∈ S) :
m.sum ∈ S
source
@[protected]
theorem subalgebra.sum_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {ι : Type w} {t : finset ι} {f : ι → A} (h : ∀ (x : ι), x ∈ t → f x ∈ S) :
t.sum (λ (x : ι), f x) ∈ S
source
@[protected]
theorem subalgebra.multiset_prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) {m : multiset A} (h : ∀ (x : A), x ∈ m → x ∈ S) :
m.prod ∈ S
source
@[protected]
theorem subalgebra.prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) {ι : Type w} {t : finset ι} {f : ι → A} (h : ∀ (x : ι), x ∈ t → f x ∈ S) :
t.prod (λ (x : ι), f x) ∈ S
source
@[protected, instance]
def subalgebra.subring_class {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] :
subring_class (subalgebra R A) A
source
@[protected]
theorem subalgebra.neg_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) :
-x ∈ S
source
@[protected]
theorem subalgebra.sub_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) {x y : A} (hx : x ∈ S) (hy : y ∈ S) :
x - y ∈ S
source
@[protected]
theorem subalgebra.zsmul_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) (n : ℤ) :
n • x ∈ S
source
@[protected]
theorem subalgebra.coe_int_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) (n : ℤ) :
↑n ∈ S
source
def subalgebra.to_add_submonoid {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
add_submonoid A

The projection from a subalgebra of A to an additive submonoid of A.

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

The projection from a subalgebra of A to a submonoid of A.

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

A subalgebra over a ring is also a subring.

Equations
source
@[simp]
theorem subalgebra.mem_to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {S : subalgebra R A} {x : A} :
x ∈ S.to_subring ↔ x ∈ S
source
@[simp]
theorem subalgebra.coe_to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
↑(S.to_subring) = ↑S
source
theorem subalgebra.to_subring_injective {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] :
function.injective subalgebra.to_subring
source
theorem subalgebra.to_subring_inj {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {S U : subalgebra R A} :
S.to_subring = U.to_subring ↔ S = U
source
@[protected, instance]
def subalgebra.inhabited {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
inhabited ↥S
Equations

subalgebras inherit structure from their subsemiring / semiring coercions.

source
@[protected, instance]
def subalgebra.to_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_comm_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) :
comm_semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
ring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) :
comm_ring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_ordered_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [ordered_semiring A] [algebra R A] (S : subalgebra R A) :
ordered_semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_strict_ordered_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [strict_ordered_semiring A] [algebra R A] (S : subalgebra R A) :
strict_ordered_semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_ordered_comm_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
ordered_comm_semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_strict_ordered_comm_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [strict_ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
strict_ordered_comm_semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_ordered_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ordered_ring A] [algebra R A] (S : subalgebra R A) :
ordered_ring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_ordered_comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ordered_comm_ring A] [algebra R A] (S : subalgebra R A) :
ordered_comm_ring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_linear_ordered_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [linear_ordered_semiring A] [algebra R A] (S : subalgebra R A) :
linear_ordered_semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_linear_ordered_comm_semiring {R : Type u_1} {A : Type u_2} [comm_semiring R] [linear_ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
linear_ordered_comm_semiring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_linear_ordered_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [linear_ordered_ring A] [algebra R A] (S : subalgebra R A) :
linear_ordered_ring ↥S
Equations
source
@[protected, instance]
def subalgebra.to_linear_ordered_comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [linear_ordered_comm_ring A] [algebra R A] (S : subalgebra R A) :
linear_ordered_comm_ring ↥S
Equations
source
def subalgebra.to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
subalgebra R A ↪o submodule R A

The forgetful map from subalgebra to submodule as an order_embedding

Equations
source
@[simp]
theorem subalgebra.mem_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x : A} :
x ∈ ⇑subalgebra.to_submodule S ↔ x ∈ S
source
@[simp]
theorem subalgebra.coe_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
↑(⇑subalgebra.to_submodule S) = ↑S

subalgebras inherit structure from their submodule coercions.

source
@[protected, instance]
def subalgebra.module' {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [semiring R'] [has_smul R' R] [module R' A] [is_scalar_tower R' R A] :
module R' ↥S
Equations
source
@[protected, instance]
def subalgebra.module {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
module R ↥S
Equations
source
@[protected, instance]
def subalgebra.is_scalar_tower {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [semiring R'] [has_smul R' R] [module R' A] [is_scalar_tower R' R A] :
is_scalar_tower R' R ↥S
source
@[protected, instance]
def subalgebra.algebra' {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [comm_semiring R'] [has_smul R' R] [algebra R' A] [is_scalar_tower R' R A] :
algebra R' ↥S
Equations
source
@[protected, instance]
def subalgebra.algebra {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
algebra R ↥S
Equations
source
@[protected, instance]
def subalgebra.no_zero_smul_divisors_bot {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [no_zero_smul_divisors R A] :
no_zero_smul_divisors R ↥S
source
@[protected]
theorem subalgebra.coe_add {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (x y : ↥S) :
↑(x + y) = ↑x + ↑y
source
@[protected]
theorem subalgebra.coe_mul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (x y : ↥S) :
↑(x * y) = ↑x * ↑y
source
@[protected]
theorem subalgebra.coe_zero {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
↑0 = 0
source
@[protected]
theorem subalgebra.coe_one {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
↑1 = 1
source
@[protected]
theorem subalgebra.coe_neg {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {S : subalgebra R A} (x : ↥S) :
↑-x = -↑x
source
@[protected]
theorem subalgebra.coe_sub {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {S : subalgebra R A} (x y : ↥S) :
↑(x - y) = ↑x - ↑y
source
@[simp, norm_cast]
theorem subalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [semiring R'] [has_smul R' R] [module R' A] [is_scalar_tower R' R A] (r : R') (x : ↥S) :
↑(r • x) = r • ↑x
source
@[simp, norm_cast]
theorem subalgebra.coe_algebra_map {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [comm_semiring R'] [has_smul R' R] [algebra R' A] [is_scalar_tower R' R A] (r : R') :
↑(⇑(algebra_map R' ↥S) r) = ⇑(algebra_map R' A) r
source
@[protected]
theorem subalgebra.coe_pow {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (x : ↥S) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
@[protected]
theorem subalgebra.coe_eq_zero {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x : ↥S} :
↑x = 0 ↔ x = 0
source
@[protected]
theorem subalgebra.coe_eq_one {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {x : ↥S} :
↑x = 1 ↔ x = 1
source
def subalgebra.val {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
↥S →ₐ[R] A

Embedding of a subalgebra into the algebra.

Equations
source
@[simp]
theorem subalgebra.coe_val {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
⇑(S.val) = coe
source
theorem subalgebra.val_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (x : ↥S) :
⇑(S.val) x = ↑x
source
@[simp]
theorem subalgebra.to_subsemiring_subtype {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
S.to_subsemiring.subtype = ↑(S.val)
source
@[simp]
theorem subalgebra.to_subring_subtype {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
S.to_subring.subtype = ↑(S.val)
source
def subalgebra.to_submodule_equiv {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
↥(⇑subalgebra.to_submodule S) ≃ₗ[R] ↥S

Linear equivalence between S : submodule R A and S. Though these types are equal, we define it as a linear_equiv to avoid type equalities.

Equations
source
def subalgebra.map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R A) :
subalgebra R B

Transport a subalgebra via an algebra homomorphism.

Equations
source
theorem subalgebra.map_mono {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S₁ S₂ : subalgebra R A} {f : A →ₐ[R] B} :
S₁ ≤ S₂ → subalgebra.map f S₁ ≤ subalgebra.map f S₂
source
theorem subalgebra.map_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {f : A →ₐ[R] B} (hf : function.injective ⇑f) :
function.injective (subalgebra.map f)
source
@[simp]
theorem subalgebra.map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
subalgebra.map (alg_hom.id R A) S = S
source
theorem subalgebra.map_map {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (S : subalgebra R A) (g : B →ₐ[R] C) (f : A →ₐ[R] B) :
subalgebra.map g (subalgebra.map f S) = subalgebra.map (g.comp f) S
source
theorem subalgebra.mem_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S : subalgebra R A} {f : A →ₐ[R] B} {y : B} :
y ∈ subalgebra.map f S ↔ ∃ (x : A) (H : x ∈ S), ⇑f x = y
source
theorem subalgebra.map_to_submodule {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S : subalgebra R A} {f : A →ₐ[R] B} :
⇑subalgebra.to_submodule (subalgebra.map f S) = submodule.map f.to_linear_map (⇑subalgebra.to_submodule S)
source
theorem subalgebra.map_to_subsemiring {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S : subalgebra R A} {f : A →ₐ[R] B} :
(subalgebra.map f S).to_subsemiring = subsemiring.map f.to_ring_hom S.to_subsemiring
source
@[simp]
theorem subalgebra.coe_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R A) (f : A →ₐ[R] B) :
↑(subalgebra.map f S) = ⇑f '' ↑S
source
def subalgebra.comap {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) :
subalgebra R A

Preimage of a subalgebra under an algebra homomorphism.

Equations
source
theorem subalgebra.map_le {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S : subalgebra R A} {f : A →ₐ[R] B} {U : subalgebra R B} :
subalgebra.map f S ≤ U ↔ S ≤ subalgebra.comap f U
source
theorem subalgebra.gc_map_comap {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :
galois_connection (subalgebra.map f) (subalgebra.comap f)
source
@[simp]
theorem subalgebra.mem_comap {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R B) (f : A →ₐ[R] B) (x : A) :
x ∈ subalgebra.comap f S ↔ ⇑f x ∈ S
source
@[simp, norm_cast]
theorem subalgebra.coe_comap {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R B) (f : A →ₐ[R] B) :
↑(subalgebra.comap f S) = ⇑f ⁻¹' ↑S
source
@[protected, instance]
def subalgebra.no_zero_divisors {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [no_zero_divisors A] [algebra R A] (S : subalgebra R A) :
no_zero_divisors ↥S
source
@[protected, instance]
def subalgebra.is_domain {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [is_domain A] [algebra R A] (S : subalgebra R A) :
is_domain ↥S
source
def submodule.to_subalgebra {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (p : submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) :
subalgebra R A

A submodule containing 1 and closed under multiplication is a subalgebra.

Equations
source
@[simp]
theorem submodule.mem_to_subalgebra {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {p : submodule R A} {h_one : 1 ∈ p} {h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p} {x : A} :
x ∈ p.to_subalgebra h_one h_mul ↔ x ∈ p
source
@[simp]
theorem submodule.coe_to_subalgebra {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (p : submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) :
↑(p.to_subalgebra h_one h_mul) = ↑p
source
@[simp]
theorem submodule.to_subalgebra_mk {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (s : set A) (h0 : 0 ∈ s) (hadd : ∀ {a b : A}, a ∈ s → b ∈ s → a + b ∈ s) (hsmul : ∀ (c : R) {x : A}, x ∈ s → c • x ∈ s) (h1 : 1 ∈ {carrier := s, add_mem' := hadd, zero_mem' := h0, smul_mem' := hsmul}) (hmul : ∀ (x y : A), x ∈ {carrier := s, add_mem' := hadd, zero_mem' := h0, smul_mem' := hsmul} → y ∈ {carrier := s, add_mem' := hadd, zero_mem' := h0, smul_mem' := hsmul} → x * y ∈ {carrier := s, add_mem' := hadd, zero_mem' := h0, smul_mem' := hsmul}) :
{carrier := s, add_mem' := hadd, zero_mem' := h0, smul_mem' := hsmul}.to_subalgebra h1 hmul = {carrier := s, mul_mem' := hmul, one_mem' := h1, add_mem' := hadd, zero_mem' := h0, algebra_map_mem' := _}
source
@[simp]
theorem submodule.to_subalgebra_to_submodule {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (p : submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) :
⇑subalgebra.to_submodule (p.to_subalgebra h_one h_mul) = p
source
@[simp]
theorem subalgebra.to_submodule_to_subalgebra {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
(⇑subalgebra.to_submodule S).to_subalgebra _ _ = S
source
@[protected]
def alg_hom.range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (φ : A →ₐ[R] B) :
subalgebra R B

Range of an alg_hom as a subalgebra.

Equations
Instances for ↥alg_hom.range
source
@[simp]
theorem alg_hom.mem_range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (φ : A →ₐ[R] B) {y : B} :
y ∈ φ.range ↔ ∃ (x : A), ⇑φ x = y
source
theorem alg_hom.mem_range_self {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
⇑φ x ∈ φ.range
source
@[simp]
theorem alg_hom.coe_range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (φ : A →ₐ[R] B) :
↑(φ.range) = set.range ⇑φ
source
theorem alg_hom.range_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
(g.comp f).range = subalgebra.map g f.range
source
theorem alg_hom.range_comp_le_range {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
(g.comp f).range ≤ g.range
source
def alg_hom.cod_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ (x : A), ⇑f x ∈ S) :
A →ₐ[R] ↥S

Restrict the codomain of an algebra homomorphism.

Equations
source
@[simp]
theorem alg_hom.val_comp_cod_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ (x : A), ⇑f x ∈ S) :
S.val.comp (f.cod_restrict S hf) = f
source
@[simp]
theorem alg_hom.coe_cod_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ (x : A), ⇑f x ∈ S) (x : A) :
↑(⇑(f.cod_restrict S hf) x) = ⇑f x
source
theorem alg_hom.injective_cod_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ (x : A), ⇑f x ∈ S) :
function.injective ⇑(f.cod_restrict S hf) ↔ function.injective ⇑f
source
@[reducible]
def alg_hom.range_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :
A →ₐ[R] ↥(f.range)

Restrict the codomain of a alg_hom f to f.range.

This is the bundled version of set.range_factorization.

Equations
source
def alg_hom.equalizer {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (ϕ ψ : A →ₐ[R] B) :
subalgebra R A

The equalizer of two R-algebra homomorphisms

Equations
source
@[simp]
theorem alg_hom.mem_equalizer {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (ϕ ψ : A →ₐ[R] B) (x : A) :
x ∈ ϕ.equalizer ψ ↔ ⇑ϕ x = ⇑ψ x
source
@[protected, instance]
def alg_hom.fintype_range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [fintype A] [decidable_eq B] (φ : A →ₐ[R] B) :
fintype ↥(φ.range)

The range of a morphism of algebras is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with subtype.fintype if B is also a fintype.

Equations
source
def alg_equiv.of_left_inverse {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : function.left_inverse g ⇑f) :
A ≃ₐ[R] ↥(f.range)

Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.

This is a computable alternative to alg_equiv.of_injective.

Equations
source
@[simp]
theorem alg_equiv.of_left_inverse_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : function.left_inverse g ⇑f) (x : A) :
↑(⇑(alg_equiv.of_left_inverse h) x) = ⇑f x
source
@[simp]
theorem alg_equiv.of_left_inverse_symm_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : function.left_inverse g ⇑f) (x : ↥(f.range)) :
⇑((alg_equiv.of_left_inverse h).symm) x = g ↑x
source
noncomputable def alg_equiv.of_injective {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) (hf : function.injective ⇑f) :
A ≃ₐ[R] ↥(f.range)

Restrict an injective algebra homomorphism to an algebra isomorphism

Equations
source
@[simp]
theorem alg_equiv.of_injective_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) (hf : function.injective ⇑f) (x : A) :
↑(⇑(alg_equiv.of_injective f hf) x) = ⇑f x
source
noncomputable def alg_equiv.of_injective_field {R : Type u} [comm_semiring R] {E : Type u_1} {F : Type u_2} [division_ring E] [semiring F] [nontrivial F] [algebra R E] [algebra R F] (f : E →ₐ[R] F) :
E ≃ₐ[R] ↥(f.range)

Restrict an algebra homomorphism between fields to an algebra isomorphism

Equations
source
@[simp]
theorem alg_equiv.subalgebra_map_symm_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) (ᾰ : ↥(subsemiring.map e.to_ring_equiv.to_ring_hom S.to_subsemiring)) :
⇑((e.subalgebra_map S).symm) ᾰ = (e.to_ring_equiv.subsemiring_map S.to_subsemiring).inv_fun ᾰ
source
@[simp]
theorem alg_equiv.subalgebra_map_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) (ᾰ : ↥(S.to_subsemiring)) :
⇑(e.subalgebra_map S) ᾰ = (e.to_ring_equiv.subsemiring_map S.to_subsemiring).to_fun ᾰ
source
def alg_equiv.subalgebra_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) :
↥S ≃ₐ[R] ↥(subalgebra.map e.to_alg_hom S)

Given an equivalence e : A ≃ₐ[R] B of R-algebras and a subalgebra S of A, subalgebra_map is the induced equivalence between S and S.map e

Equations
source
def algebra.adjoin (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
subalgebra R A

The minimal subalgebra that includes s.

Equations
source
@[protected]
theorem algebra.gc {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
galois_connection (algebra.adjoin R) coe
source
@[protected]
def algebra.gi {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
galois_insertion (algebra.adjoin R) coe

Galois insertion between adjoin and coe.

Equations
source
@[protected, instance]
def algebra.subalgebra.complete_lattice {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
complete_lattice (subalgebra R A)
Equations
source
@[simp]
theorem algebra.coe_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
↑⊤ = set.univ
source
@[simp]
theorem algebra.mem_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {x : A} :
x ∈ ⊤
source
@[simp]
theorem algebra.top_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
⇑subalgebra.to_submodule ⊤ = ⊤
source
@[simp]
theorem algebra.top_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
⊤.to_subsemiring = ⊤
source
@[simp]
theorem algebra.top_to_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] :
⊤.to_subring = ⊤
source
@[simp]
theorem algebra.to_submodule_eq_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : subalgebra R A} :
⇑subalgebra.to_submodule S = ⊤ ↔ S = ⊤
source
@[simp]
theorem algebra.to_subsemiring_eq_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : subalgebra R A} :
S.to_subsemiring = ⊤ ↔ S = ⊤
source
@[simp]
theorem algebra.to_subring_eq_top {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] {S : subalgebra R A} :
S.to_subring = ⊤ ↔ S = ⊤
source
theorem algebra.mem_sup_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} {x : A} :
x ∈ S → x ∈ S ⊔ T
source
theorem algebra.mem_sup_right {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} {x : A} :
x ∈ T → x ∈ S ⊔ T
source
theorem algebra.mul_mem_sup {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) :
x * y ∈ S ⊔ T
source
theorem algebra.map_sup {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) (S T : subalgebra R A) :
subalgebra.map f (S ⊔ T) = subalgebra.map f S ⊔ subalgebra.map f T
source
@[simp, norm_cast]
theorem algebra.coe_inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) :
↑(S ⊓ T) = ↑S ∩ ↑T
source
@[simp]
theorem algebra.mem_inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} {x : A} :
x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
source
@[simp]
theorem algebra.inf_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) :
⇑subalgebra.to_submodule (S ⊓ T) = ⇑subalgebra.to_submodule S ⊓ ⇑subalgebra.to_submodule T
source
@[simp]
theorem algebra.inf_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) :
(S ⊓ T).to_subsemiring = S.to_subsemiring ⊓ T.to_subsemiring
source
@[simp, norm_cast]
theorem algebra.coe_Inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : set (subalgebra R A)) :
↑(has_Inf.Inf S) = ⋂ (s : subalgebra R A) (H : s ∈ S), ↑s
source
theorem algebra.mem_Inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : set (subalgebra R A)} {x : A} :
x ∈ has_Inf.Inf S ↔ ∀ (p : subalgebra R A), p ∈ S → x ∈ p
source
@[simp]
theorem algebra.Inf_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : set (subalgebra R A)) :
⇑subalgebra.to_submodule (has_Inf.Inf S) = has_Inf.Inf (⇑subalgebra.to_submodule '' S)
source
@[simp]
theorem algebra.Inf_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : set (subalgebra R A)) :
(has_Inf.Inf S).to_subsemiring = has_Inf.Inf (subalgebra.to_subsemiring '' S)
source
@[simp, norm_cast]
theorem algebra.coe_infi {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Sort u_1} {S : ι → subalgebra R A} :
(↑⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
source
theorem algebra.mem_infi {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Sort u_1} {S : ι → subalgebra R A} {x : A} :
(x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i
source
@[simp]
theorem algebra.infi_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Sort u_1} (S : ι → subalgebra R A) :
⇑subalgebra.to_submodule (⨅ (i : ι), S i) = ⨅ (i : ι), ⇑subalgebra.to_submodule (S i)
source
@[protected, instance]
def algebra.subalgebra.inhabited {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
inhabited (subalgebra R A)
Equations
source
theorem algebra.mem_bot {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {x : A} :
x ∈ ⊥ ↔ x ∈ set.range ⇑(algebra_map R A)
source
theorem algebra.to_submodule_bot {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
⇑subalgebra.to_submodule ⊥ = submodule.span R {1}
source
@[simp]
theorem algebra.coe_bot {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
↑⊥ = set.range ⇑(algebra_map R A)
source
theorem algebra.eq_top_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : subalgebra R A} :
S = ⊤ ↔ ∀ (x : A), x ∈ S
source
theorem algebra.range_top_iff_surjective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :
f.range = ⊤ ↔ function.surjective ⇑f
source
@[simp]
theorem algebra.range_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
(alg_hom.id R A).range = ⊤
source
@[simp]
theorem algebra.map_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :
subalgebra.map f ⊤ = f.range
source
@[simp]
theorem algebra.map_bot {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :
subalgebra.map f ⊥ = ⊥
source
@[simp]
theorem algebra.comap_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :
subalgebra.comap f ⊤ = ⊤
source
def algebra.to_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
A →ₐ[R] ↥⊤

alg_hom to ⊤ : subalgebra R A.

Equations
source
theorem algebra.surjective_algebra_map_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
function.surjective ⇑(algebra_map R A) ↔ ⊤ = ⊥
source
theorem algebra.bijective_algebra_map_iff {R : Type u_1} {A : Type u_2} [field R] [semiring A] [nontrivial A] [algebra R A] :
function.bijective ⇑(algebra_map R A) ↔ ⊤ = ⊥
source
noncomputable def algebra.bot_equiv_of_injective {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (h : function.injective ⇑(algebra_map R A)) :
↥⊥ ≃ₐ[R] R

The bottom subalgebra is isomorphic to the base ring.

Equations
source
noncomputable def algebra.bot_equiv (F : Type u_1) (R : Type u_2) [field F] [semiring R] [nontrivial R] [algebra F R] :
↥⊥ ≃ₐ[F] F

The bottom subalgebra is isomorphic to the field.

Equations
source
@[simp]
theorem algebra.bot_equiv_symm_apply (F : Type u_1) (R : Type u_2) [field F] [semiring R] [nontrivial R] [algebra F R] (ᾰ : F) :
⇑((algebra.bot_equiv F R).symm) ᾰ = ⇑(algebra.of_id F ↥⊥) ᾰ
source
@[simp]
theorem subalgebra.top_equiv_symm_apply_coe {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (ᾰ : A) :
↑(⇑(subalgebra.top_equiv.symm) ᾰ) = ᾰ
source
@[simp]
theorem subalgebra.top_equiv_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (ᾰ : ↥⊤) :
⇑subalgebra.top_equiv ᾰ = ↑ᾰ
source
def subalgebra.top_equiv {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
↥⊤ ≃ₐ[R] A

The top subalgebra is isomorphic to the algebra.

This is the algebra version of submodule.top_equiv.

Equations
source
@[protected, instance]
def subalgebra.subsingleton_of_subsingleton {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] [subsingleton A] :
subsingleton (subalgebra R A)
source
@[protected, instance]
def alg_hom.subsingleton {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [subsingleton (subalgebra R A)] :
subsingleton (A →ₐ[R] B)
source
@[protected, instance]
def alg_equiv.subsingleton_left {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [subsingleton (subalgebra R A)] :
subsingleton (A ≃ₐ[R] B)
source
@[protected, instance]
def alg_equiv.subsingleton_right {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [subsingleton (subalgebra R B)] :
subsingleton (A ≃ₐ[R] B)
source
theorem subalgebra.range_val {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
S.val.range = S
source
@[protected, instance]
def subalgebra.unique {R : Type u} [comm_semiring R] :
unique (subalgebra R R)
Equations
source
def subalgebra.inclusion {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) :
↥S →ₐ[R] ↥T

The map S → T when S is a subalgebra contained in the subalgebra T.

This is the subalgebra version of submodule.of_le, or subring.inclusion

Equations
source
theorem subalgebra.inclusion_injective {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) :
function.injective ⇑(subalgebra.inclusion h)
source
@[simp]
theorem subalgebra.inclusion_self {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : subalgebra R A} :
subalgebra.inclusion _ = alg_hom.id R ↥S
source
@[simp]
theorem subalgebra.inclusion_mk {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) :
⇑(subalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, _⟩
source
theorem subalgebra.inclusion_right {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S) :
⇑(subalgebra.inclusion h) ⟨↑x, m⟩ = x
source
@[simp]
theorem subalgebra.inclusion_inclusion {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T U : subalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S) :
⇑(subalgebra.inclusion htu) (⇑(subalgebra.inclusion hst) x) = ⇑(subalgebra.inclusion _) x
source
@[simp]
theorem subalgebra.coe_inclusion {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) (s : ↥S) :
↑(⇑(subalgebra.inclusion h) s) = ↑s
source
def subalgebra.equiv_of_eq {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) (h : S = T) :
↥S ≃ₐ[R] ↥T

Two subalgebras that are equal are also equivalent as algebras.

This is the subalgebra version of linear_equiv.of_eq and equiv.set.of_eq.

Equations
source
@[simp]
theorem subalgebra.equiv_of_eq_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) (h : S = T) (x : ↥S) :
⇑(S.equiv_of_eq T h) x = ⟨↑x, _⟩
source
@[simp]
theorem subalgebra.equiv_of_eq_symm {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) (h : S = T) :
(S.equiv_of_eq T h).symm = T.equiv_of_eq S _
source
@[simp]
theorem subalgebra.equiv_of_eq_rfl {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
S.equiv_of_eq S rfl = alg_equiv.refl
source
@[simp]
theorem subalgebra.equiv_of_eq_trans {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T U : subalgebra R A) (hST : S = T) (hTU : T = U) :
(S.equiv_of_eq T hST).trans (T.equiv_of_eq U hTU) = S.equiv_of_eq U _
source
def subalgebra.prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R A) (S₁ : subalgebra R B) :
subalgebra R (A × B)

The product of two subalgebras is a subalgebra.

Equations
source
@[simp]
theorem subalgebra.coe_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R A) (S₁ : subalgebra R B) :
↑(S.prod S₁) = ↑S ×ˢ ↑S₁
source
theorem subalgebra.prod_to_submodule {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R A) (S₁ : subalgebra R B) :
⇑subalgebra.to_submodule (S.prod S₁) = (⇑subalgebra.to_submodule S).prod (⇑subalgebra.to_submodule S₁)
source
@[simp]
theorem subalgebra.mem_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S : subalgebra R A} {S₁ : subalgebra R B} {x : A × B} :
x ∈ S.prod S₁ ↔ x.fst ∈ S ∧ x.snd ∈ S₁
source
@[simp]
theorem subalgebra.prod_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :
⊤.prod ⊤ = ⊤
source
theorem subalgebra.prod_mono {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S T : subalgebra R A} {S₁ T₁ : subalgebra R B} :
S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
source
@[simp]
theorem subalgebra.prod_inf_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S T : subalgebra R A} {S₁ T₁ : subalgebra R B} :
S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
source
theorem subalgebra.coe_supr_of_directed {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Type u_1} [nonempty ι] {S : ι → subalgebra R A} (dir : directed has_le.le S) :
↑(supr S) = ⋃ (i : ι), ↑(S i)
source
noncomputable def subalgebra.supr_lift {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] (K : ι → subalgebra R A) (dir : directed has_le.le K) (f : Π (i : ι), ↥(K i) →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)) (T : subalgebra R A) (hT : T = supr K) :
↥T →ₐ[R] B

Define an algebra homomorphism on a directed supremum of subalgebras by defining it on each subalgebra, and proving that it agrees on the intersection of subalgebras.

Equations
source
@[simp]
theorem subalgebra.supr_lift_inclusion {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] {K : ι → subalgebra R A} {dir : directed has_le.le K} {f : Π (i : ι), ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)} {T : subalgebra R A} {hT : T = supr K} {i : ι} (x : ↥(K i)) (h : K i ≤ T) :
⇑(subalgebra.supr_lift K dir f hf T hT) (⇑(subalgebra.inclusion h) x) = ⇑(f i) x
source
@[simp]
theorem subalgebra.supr_lift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] {K : ι → subalgebra R A} {dir : directed has_le.le K} {f : Π (i : ι), ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)} {T : subalgebra R A} {hT : T = supr K} {i : ι} (h : K i ≤ T) :
(subalgebra.supr_lift K dir f hf T hT).comp (subalgebra.inclusion h) = f i
source
@[simp]
theorem subalgebra.supr_lift_mk {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] {K : ι → subalgebra R A} {dir : directed has_le.le K} {f : Π (i : ι), ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)} {T : subalgebra R A} {hT : T = supr K} {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T) :
⇑(subalgebra.supr_lift K dir f hf T hT) ⟨↑x, hx⟩ = ⇑(f i) x
source
theorem subalgebra.supr_lift_of_mem {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] {K : ι → subalgebra R A} {dir : directed has_le.le K} {f : Π (i : ι), ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)} {T : subalgebra R A} {hT : T = supr K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i) :
⇑(subalgebra.supr_lift K dir f hf T hT) x = ⇑(f i) ⟨↑x, hx⟩

Actions by subalgebras #

These are just copies of the definitions about subsemiring starting from subring.mul_action.

source
@[protected, instance]
def subalgebra.has_smul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [has_smul A α] (S : subalgebra R A) :
has_smul ↥S α

The action by a subalgebra is the action by the underlying algebra.

Equations
source
theorem subalgebra.smul_def {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [has_smul A α] {S : subalgebra R A} (g : ↥S) (m : α) :
g • m = ↑g • m
source
@[protected, instance]
def subalgebra.smul_comm_class_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} {β : Type u_2} [has_smul A β] [has_smul α β] [smul_comm_class A α β] (S : subalgebra R A) :
smul_comm_class ↥S α β
source
@[protected, instance]
def subalgebra.smul_comm_class_right {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} {β : Type u_2} [has_smul α β] [has_smul A β] [smul_comm_class α A β] (S : subalgebra R A) :
smul_comm_class α ↥S β
source
@[protected, instance]
def subalgebra.is_scalar_tower_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} {β : Type u_2} [has_smul α β] [has_smul A α] [has_smul A β] [is_scalar_tower A α β] (S : subalgebra R A) :
is_scalar_tower ↥S α β

Note that this provides is_scalar_tower S R R which is needed by smul_mul_assoc.

source
@[protected, instance]
def subalgebra.is_scalar_tower_mid {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_semiring R] [semiring S] [add_comm_monoid T] [algebra R S] [module R T] [module S T] [is_scalar_tower R S T] (S' : subalgebra R S) :
is_scalar_tower R ↥S' T
source
@[protected, instance]
def subalgebra.has_faithful_smul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [has_smul A α] [has_faithful_smul A α] (S : subalgebra R A) :
has_faithful_smul ↥S α
source
@[protected, instance]
def subalgebra.mul_action {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [mul_action A α] (S : subalgebra R A) :
mul_action ↥S α

The action by a subalgebra is the action by the underlying algebra.

Equations
source
@[protected, instance]
def subalgebra.distrib_mul_action {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [add_monoid α] [distrib_mul_action A α] (S : subalgebra R A) :
distrib_mul_action ↥S α

The action by a subalgebra is the action by the underlying algebra.

Equations
source
@[protected, instance]
def subalgebra.smul_with_zero {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [has_zero α] [smul_with_zero A α] (S : subalgebra R A) :
smul_with_zero ↥S α

The action by a subalgebra is the action by the underlying algebra.

Equations
source
@[protected, instance]
def subalgebra.mul_action_with_zero {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [has_zero α] [mul_action_with_zero A α] (S : subalgebra R A) :
mul_action_with_zero ↥S α

The action by a subalgebra is the action by the underlying algebra.

Equations
source
@[protected, instance]
def subalgebra.module_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [add_comm_monoid α] [module A α] (S : subalgebra R A) :
module ↥S α

The action by a subalgebra is the action by the underlying algebra.

Equations
source
@[protected, instance]
def subalgebra.to_algebra {α : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [semiring α] [algebra R A] [algebra A α] (S : subalgebra R A) :
algebra ↥S α

The action by a subalgebra is the action by the underlying algebra.

Equations
source
theorem subalgebra.algebra_map_eq {α : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [semiring α] [algebra R A] [algebra A α] (S : subalgebra R A) :
algebra_map ↥S α = (algebra_map A α).comp ↑(S.val)
source
@[simp]
theorem subalgebra.srange_algebra_map {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) :
(algebra_map ↥S A).srange = S.to_subsemiring
source
@[simp]
theorem subalgebra.range_algebra_map {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) :
(algebra_map ↥S A).range = S.to_subring
source
@[protected, instance]
def subalgebra.no_zero_smul_divisors_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] [no_zero_divisors A] (S : subalgebra R A) :
no_zero_smul_divisors ↥S A
source
theorem set.algebra_map_mem_center {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (r : R) :
⇑(algebra_map R A) r ∈ set.center A
source
def subalgebra.center (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
subalgebra R A

The center of an algebra is the set of elements which commute with every element. They form a subalgebra.

Equations
Instances for ↥subalgebra.center
source
theorem subalgebra.coe_center (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
↑(subalgebra.center R A) = set.center A
source
@[simp]
theorem subalgebra.center_to_subsemiring (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
(subalgebra.center R A).to_subsemiring = subsemiring.center A
source
@[simp]
theorem subalgebra.center_to_subring (R : Type u_1) (A : Type u_2) [comm_ring R] [ring A] [algebra R A] :
(subalgebra.center R A).to_subring = subring.center A
source
@[simp]
theorem subalgebra.center_eq_top (R : Type u) [comm_semiring R] (A : Type u_1) [comm_semiring A] [algebra R A] :
subalgebra.center R A = ⊤
source
@[protected, instance]
def subalgebra.center.comm_semiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
comm_semiring ↥(subalgebra.center R A)
Equations
source
@[protected, instance]
def subalgebra.center.comm_ring {R : Type u} [comm_semiring R] {A : Type u_1} [ring A] [algebra R A] :
comm_ring ↥(subalgebra.center R A)
Equations
source
theorem subalgebra.mem_center_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {a : A} :
a ∈ subalgebra.center R A ↔ ∀ (b : A), b * a = a * b
source
@[simp]
theorem set.algebra_map_mem_centralizer {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} (r : R) :
⇑(algebra_map R A) r ∈ s.centralizer
source
def subalgebra.centralizer (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
subalgebra R A

The centralizer of a set as a subalgebra.

Equations
source
@[simp, norm_cast]
theorem subalgebra.coe_centralizer (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
↑(subalgebra.centralizer R s) = s.centralizer
source
theorem subalgebra.mem_centralizer_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {z : A} :
z ∈ subalgebra.centralizer R s ↔ ∀ (g : A), g ∈ s → g * z = z * g
source
theorem subalgebra.center_le_centralizer (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
subalgebra.center R A ≤ subalgebra.centralizer R s
source
theorem subalgebra.centralizer_le (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s t : set A) (h : s ⊆ t) :
subalgebra.centralizer R t ≤ subalgebra.centralizer R s
source
@[simp]
theorem subalgebra.centralizer_eq_top_iff_subset (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :
subalgebra.centralizer R s = ⊤ ↔ s ⊆ ↑(subalgebra.center R A)
source
@[simp]
theorem subalgebra.centralizer_univ (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
subalgebra.centralizer R set.univ = subalgebra.center R A
source
theorem subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem {R : Type u} [comm_semiring R] {S : Type u_1} [comm_ring S] [algebra R S] (S' : subalgebra R S) {ι : Type u_2} (ι' : finset ι) (s l : ι → S) (e : ι'.sum (λ (i : ι), l i * s i) = 1) (hs : ∀ (i : ι), s i ∈ S') (hl : ∀ (i : ι), l i ∈ S') (x : S) (H : ∀ (i : ι), ∃ (n : ℕ), s i ^ n • x ∈ S') :
x ∈ S'

Suppose we are given ∑ i, lᵢ * sᵢ = 1 in S, and S' a subalgebra of S that contains lᵢ and sᵢ. To check that an x : S falls in S', we only need to show that r ^ n • x ∈ M' for some n for each r : s.

source
theorem subalgebra.mem_of_span_eq_top_of_smul_pow_mem {R : Type u} [comm_semiring R] {S : Type u_1} [comm_ring S] [algebra R S] (S' : subalgebra R S) (s : set S) (l : ↥s →₀ S) (hs : ⇑(finsupp.total ↥s S S coe) l = 1) (hs' : s ⊆ ↑S') (hl : ∀ (i : ↥s), ⇑l i ∈ S') (x : S) (H : ∀ (r : ↥s), ∃ (n : ℕ), ↑r ^ n • x ∈ S') :
x ∈ S'
source
def subalgebra_of_subsemiring {R : Type u_1} [semiring R] (S : subsemiring R) :
subalgebra ℕ R

A subsemiring is a ℕ-subalgebra.

Equations
source
@[simp]
theorem mem_subalgebra_of_subsemiring {R : Type u_1} [semiring R] {x : R} {S : subsemiring R} :
x ∈ subalgebra_of_subsemiring S ↔ x ∈ S
source
def subalgebra_of_subring {R : Type u_1} [ring R] (S : subring R) :
subalgebra ℤ R

A subring is a ℤ-subalgebra.

Equations
source
@[simp]
theorem mem_subalgebra_of_subring {R : Type u_1} [ring R] {x : R} {S : subring R} :
x ∈ subalgebra_of_subring S ↔ x ∈ S