mathlib documentation

algebra.algebra.subalgebra

Subalgebras over Commutative Semiring #

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.

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
@[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
@[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 submodule with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
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.one_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
1 ∈ S
source
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
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
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
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
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
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
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
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
theorem subalgebra.gsmul_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) (n : ℤ) :
n • x ∈ S
source
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
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
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
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
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
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
theorem subalgebra.prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) {ι : Type w} {t : finset ι} {f : ι → A} (h : ∀ (x : ι), x ∈ t → f x ∈ S) :
∏ (x : ι) in t, f x ∈ S
source
theorem subalgebra.sum_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) {ι : Type w} {t : finset ι} {f : ι → A} (h : ∀ (x : ι), x ∈ t → f x ∈ S) :
∑ (x : ι) in t, f x ∈ S
source
@[protected, instance]
def subalgebra.is_add_submonoid {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
is_add_submonoid ↑S
source
@[protected, instance]
def subalgebra.is_submonoid {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
is_submonoid ↑S
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
@[protected, instance]
def subalgebra.is_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
is_subring ↑S
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_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_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

There is no linear_ordered_comm_semiring.

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
@[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.to_algebra {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [comm_semiring A] [semiring B] [algebra R A] [algebra A B] (A₀ : subalgebra R A) :
algebra ↥A₀ B
Equations
source
@[protected, instance]
def subalgebra.nontrivial {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [nontrivial A] :
nontrivial ↥S
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
@[simp, norm_cast]
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
@[simp, norm_cast]
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
@[simp, norm_cast]
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
@[simp, norm_cast]
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
@[simp, norm_cast]
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
@[simp, norm_cast]
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} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (r : R) (x : ↥S) :
↑(r • x) = r • ↑x
source
@[simp, norm_cast]
theorem subalgebra.coe_algebra_map {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (r : R) :
↑(⇑(algebra_map R ↥S) r) = ⇑(algebra_map R A) r
source
@[simp, norm_cast]
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
@[simp, norm_cast]
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
@[simp, norm_cast]
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
def subalgebra.to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
submodule R A

Convert a subalgebra to submodule

Equations
source
@[protected, instance]
def subalgebra.to_submodule.is_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
is_subring ↑(S.to_submodule)
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 ∈ S.to_submodule ↔ x ∈ S
source
theorem subalgebra.to_submodule_injective {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
function.injective subalgebra.to_submodule
source
theorem subalgebra.to_submodule_inj {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S U : subalgebra R A} :
S.to_submodule = U.to_submodule ↔ S = U
source
@[simp]
theorem subalgebra.mul_self {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
(S.to_submodule) * S.to_submodule = S.to_submodule

As submodules, subalgebras are idempotent.

source
def subalgebra.to_submodule_equiv {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
↥(S.to_submodule) ≃ₗ[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.comap {R : Type u} {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] (iSB : subalgebra S A) :
subalgebra R (algebra.comap R S A)

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

Equations
source
def subalgebra.under {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A] {i : algebra R A} (S : subalgebra R A) (T : subalgebra ↥S A) :
subalgebra R A

If S is an R-subalgebra of A and T is an S-subalgebra of A, then T is an R-subalgebra of A.

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] (S : subalgebra R A) (f : A →ₐ[R] B) :
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₂ → S₁.map f ≤ S₂.map f
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] {S₁ S₂ : subalgebra R A} (f : A →ₐ[R] B) (hf : function.injective ⇑f) (ih : S₁.map f = S₂.map f) :
S₁ = 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 ∈ S.map f ↔ ∃ (x : A) (H : x ∈ S), ⇑f x = y
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] (S : subalgebra R B) (f : A →ₐ[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} :
S.map f ≤ U ↔ S ≤ U.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 ∈ S.comap' f ↔ ⇑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) :
↑(S.comap' f) = ⇑f ⁻¹' ↑S
source
@[protected, instance]
def subalgebra.no_zero_divisors {R : Type u_1} {A : Type u_2} [comm_ring R] [semiring A] [no_zero_divisors A] [algebra R A] (S : subalgebra R A) :
no_zero_divisors ↥S
source
@[protected, instance]
def subalgebra.no_zero_smul_divisors_top {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] [no_zero_divisors A] (S : subalgebra R A) :
no_zero_smul_divisors ↥S A
source
@[protected, instance]
def subalgebra.integral_domain {R : Type u_1} {A : Type u_2} [comm_ring R] [integral_domain A] [algebra R A] (S : subalgebra R A) :
integral_domain ↥S
Equations
source
@[protected]
def alg_hom.range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
subalgebra R B

Range of an alg_hom as a subalgebra.

Equations
source
@[simp]
theorem alg_hom.mem_range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {y : B} :
y ∈ φ.range ↔ ∃ (x : A), ⇑φ x = y
source
theorem alg_hom.mem_range_self {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 ∈ φ.range
source
@[simp]
theorem alg_hom.coe_range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
↑(φ.range) = set.range ⇑φ
source
def alg_hom.cod_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ (x : A), ⇑f x ∈ S) :
A →ₐ[R] ↥S

Restrict the codomain of an algebra homomorphism.

Equations
source
@[simp]
theorem alg_hom.val_comp_cod_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ (x : A), ⇑f x ∈ S) :
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] [semiring B] [algebra R A] [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] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ (x : A), ⇑f x ∈ S) :
function.injective ⇑(f.cod_restrict S hf) ↔ function.injective ⇑f
source
def alg_hom.range_restrict {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
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] [semiring B] [algebra R A] [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] [semiring B] [algebra R A] [algebra R B] (ϕ ψ : A →ₐ[R] B) (x : A) :
x ∈ ϕ.equalizer ψ ↔ ⇑ϕ x = ⇑ψ x
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
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
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
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
@[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] :
⊥.to_submodule = submodule.span R {1}
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] :
⊤.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.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
@[simp]
theorem algebra.map_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :
⊤.map f = f.range
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) :
⊥.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) :
⊤.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
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
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
def algebra.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 field.

Equations
source
theorem 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
theorem subalgebra.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
theorem subalgebra.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
theorem subalgebra.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_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
def subalgebra_of_is_subring {R : Type u_1} [ring R] (S : set R) [is_subring S] :
subalgebra ℤ R

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

Equations
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
source
@[simp]
theorem mem_subalgebra_of_is_subring {R : Type u_1} [ring R] {x : R} {S : set R} [is_subring S] :
x ∈ subalgebra_of_is_subring S ↔ x ∈ S