# mathlibdocumentation

algebra.algebra.subalgebra.basic

# Subalgebras over Commutative Semiring #

In this file we define `subalgebra`s and the usual operations on them (`map`, `comap'`).

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

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

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

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

Reinterpret a `subalgebra` as a `subsemiring`.

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

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

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

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

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

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

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

A subalgebra over a ring is also a `subring`.

Equations
@[simp]
theorem subalgebra.mem_to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {S : A} {x : A} :
@[simp]
theorem subalgebra.coe_to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) :
theorem subalgebra.to_subring_injective {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] :
theorem subalgebra.to_subring_inj {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {S U : A} :
S = U
@[protected, instance]
def subalgebra.inhabited {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
Equations

`subalgebra`s inherit structure from their `subsemiring` / `semiring` coercions.

@[protected, instance]
def subalgebra.to_semiring {R : Type u_1} {A : Type u_2} [semiring A] [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_comm_semiring {R : Type u_1} {A : Type u_2} [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_ordered_semiring {R : Type u_1} {A : Type u_2} [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_ordered_comm_semiring {R : Type u_1} {A : Type u_2} [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_ordered_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ordered_ring A] [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_ordered_comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_linear_ordered_semiring {R : Type u_1} {A : Type u_2} [ A] (S : A) :
Equations

There is no `linear_ordered_comm_semiring`.

@[protected, instance]
def subalgebra.to_linear_ordered_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ A] (S : A) :
Equations
@[protected, instance]
def subalgebra.to_linear_ordered_comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [ A] (S : A) :
Equations
def subalgebra.to_submodule {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
A

Convert a `subalgebra` to `submodule`

Equations
@[simp]
theorem subalgebra.mem_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] (S : A) {x : A} :
x S
@[simp]
theorem subalgebra.coe_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
theorem subalgebra.to_submodule_injective {R : Type u} {A : Type v} [semiring A] [ A] :
theorem subalgebra.to_submodule_inj {R : Type u} {A : Type v} [semiring A] [ A] {S U : A} :
S = U

`subalgebra`s inherit structure from their `submodule` coercions.

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

Embedding of a subalgebra into the algebra.

Equations
@[simp]
theorem subalgebra.coe_val {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
theorem subalgebra.val_apply {R : Type u} {A : Type v} [semiring A] [ A] (S : A) (x : S) :
(S.val) x = x
@[simp]
theorem subalgebra.to_subsemiring_subtype {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
@[simp]
theorem subalgebra.to_subring_subtype {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] (S : A) :
def subalgebra.to_submodule_equiv {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :

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
def subalgebra.map {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : A) (f : A →ₐ[R] B) :
B

Transport a subalgebra via an algebra homomorphism.

Equations
theorem subalgebra.map_mono {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S₁ S₂ : A} {f : A →ₐ[R] B} :
S₁ S₂S₁.map f S₂.map f
theorem subalgebra.map_injective {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S₁ S₂ : A} (f : A →ₐ[R] B) (hf : function.injective f) (ih : S₁.map f = S₂.map f) :
S₁ = S₂
@[simp]
theorem subalgebra.map_id {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
S.map A) = S
theorem subalgebra.map_map {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [semiring A] [ A] [semiring B] [ B] [semiring C] [ C] (S : A) (g : B →ₐ[R] C) (f : A →ₐ[R] B) :
(S.map f).map g = S.map (g.comp f)
theorem subalgebra.mem_map {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S : A} {f : A →ₐ[R] B} {y : B} :
y S.map f ∃ (x : A) (H : x S), f x = y
theorem subalgebra.map_to_submodule {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S : A} {f : A →ₐ[R] B} :
theorem subalgebra.map_to_subsemiring {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S : A} {f : A →ₐ[R] B} :
@[simp]
theorem subalgebra.coe_map {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : A) (f : A →ₐ[R] B) :
(S.map f) = f '' S
def subalgebra.comap' {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : B) (f : A →ₐ[R] B) :
A

Preimage of a subalgebra under an algebra homomorphism.

Equations
theorem subalgebra.map_le {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S : A} {f : A →ₐ[R] B} {U : B} :
S.map f U S U.comap' f
theorem subalgebra.gc_map_comap {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) :
galois_connection (λ (S : A), S.map f) (λ (S : B), S.comap' f)
@[simp]
theorem subalgebra.mem_comap {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : B) (f : A →ₐ[R] B) (x : A) :
x S.comap' f f x S
@[simp, norm_cast]
theorem subalgebra.coe_comap {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : B) (f : A →ₐ[R] B) :
@[protected, instance]
def subalgebra.no_zero_divisors {R : Type u_1} {A : Type u_2} [semiring A] [ A] (S : A) :
@[protected, instance]
def subalgebra.is_domain {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [is_domain A] [ A] (S : A) :
def submodule.to_subalgebra {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : A) (h_one : 1 p) (h_mul : ∀ (x y : A), x py px * y p) :
A

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

Equations
@[simp]
theorem submodule.mem_to_subalgebra {R : Type u_1} {A : Type u_2} [semiring A] [ A] {p : A} {h_one : 1 p} {h_mul : ∀ (x y : A), x py px * y p} {x : A} :
x p.to_subalgebra h_one h_mul x p
@[simp]
theorem submodule.coe_to_subalgebra {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : A) (h_one : 1 p) (h_mul : ∀ (x y : A), x py px * y p) :
(p.to_subalgebra h_one h_mul) = p
@[simp]
theorem submodule.to_subalgebra_mk {R : Type u_1} {A : Type u_2} [semiring A] [ A] (s : set A) (h0 : 0 s) (hadd : ∀ {a b : A}, a sb sa + b s) (hsmul : ∀ (c : R) {x : A}, x sc 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' := _}
@[simp]
theorem submodule.to_subalgebra_to_submodule {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : A) (h_one : 1 p) (h_mul : ∀ (x y : A), x py px * y p) :
(p.to_subalgebra h_one h_mul).to_submodule = p
@[simp]
theorem subalgebra.to_submodule_to_subalgebra {R : Type u_1} {A : Type u_2} [semiring A] [ A] (S : A) :
= S
@[protected]
def alg_hom.range {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (φ : A →ₐ[R] B) :
B

Range of an `alg_hom` as a subalgebra.

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

Restrict the codomain of an algebra homomorphism.

Equations
@[simp]
theorem alg_hom.val_comp_cod_restrict {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) (S : B) (hf : ∀ (x : A), f x S) :
S.val.comp (f.cod_restrict S hf) = f
@[simp]
theorem alg_hom.coe_cod_restrict {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) (S : B) (hf : ∀ (x : A), f x S) (x : A) :
((f.cod_restrict S hf) x) = f x
theorem alg_hom.injective_cod_restrict {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) (S : B) (hf : ∀ (x : A), f x S) :
def alg_hom.range_restrict {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) :

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

This is the bundled version of `set.range_factorization`.

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

The equalizer of two R-algebra homomorphisms

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

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
def alg_equiv.of_left_inverse {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] {g : B → A} {f : A →ₐ[R] B} (h : f) :

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

Restrict an injective algebra homomorphism to an algebra isomorphism

Equations
@[simp]
theorem alg_equiv.of_injective_apply {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) (hf : function.injective f) (x : A) :
( hf) x) = f x
noncomputable def alg_equiv.of_injective_field {R : Type u} {E : Type u_1} {F : Type u_2} [semiring F] [nontrivial F] [ E] [ F] (f : E →ₐ[R] F) :

Restrict an algebra homomorphism between fields to an algebra isomorphism

Equations
@[simp]
theorem alg_equiv.subalgebra_map_symm_apply {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (e : A ≃ₐ[R] B) (S : A) (ᾰ : ) :
((e.subalgebra_map S).symm) =
@[simp]
theorem alg_equiv.subalgebra_map_apply {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (e : A ≃ₐ[R] B) (S : A) (ᾰ : (S.to_subsemiring)) :
(e.subalgebra_map S) =
def alg_equiv.subalgebra_map {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (e : A ≃ₐ[R] B) (S : A) :

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
def algebra.adjoin (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) :
A

The minimal subalgebra that includes `s`.

Equations
@[protected]
theorem algebra.gc {R : Type u} {A : Type v} [semiring A] [ A] :
@[protected]
def algebra.gi {R : Type u} {A : Type v} [semiring A] [ A] :

Galois insertion between `adjoin` and `coe`.

Equations
@[protected, instance]
def algebra.subalgebra.complete_lattice {R : Type u} {A : Type v} [semiring A] [ A] :
Equations
@[simp]
theorem algebra.coe_top {R : Type u} {A : Type v} [semiring A] [ A] :
@[simp]
theorem algebra.mem_top {R : Type u} {A : Type v} [semiring A] [ A] {x : A} :
@[simp]
theorem algebra.top_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] :
@[simp]
theorem algebra.top_to_subsemiring {R : Type u} {A : Type v} [semiring A] [ A] :
@[simp]
theorem algebra.top_to_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] :
@[simp]
theorem algebra.to_submodule_eq_top {R : Type u} {A : Type v} [semiring A] [ A] {S : A} :
S =
@[simp]
theorem algebra.to_subsemiring_eq_top {R : Type u} {A : Type v} [semiring A] [ A] {S : A} :
S =
@[simp]
theorem algebra.to_subring_eq_top {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {S : A} :
S =
theorem algebra.mem_sup_left {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} {x : A} :
x Sx S T
theorem algebra.mem_sup_right {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} {x : A} :
x Tx S T
theorem algebra.mul_mem_sup {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} {x y : A} (hx : x S) (hy : y T) :
x * y S T
theorem algebra.map_sup {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) (S T : A) :
(S T).map f = S.map f T.map f
@[simp, norm_cast]
theorem algebra.coe_inf {R : Type u} {A : Type v} [semiring A] [ A] (S T : A) :
(S T) = S T
@[simp]
theorem algebra.mem_inf {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} {x : A} :
x S T x S x T
@[simp]
theorem algebra.inf_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] (S T : A) :
@[simp]
theorem algebra.inf_to_subsemiring {R : Type u} {A : Type v} [semiring A] [ A] (S T : A) :
@[simp, norm_cast]
theorem algebra.coe_Inf {R : Type u} {A : Type v} [semiring A] [ A] (S : set A)) :
(has_Inf.Inf S) = ⋂ (s : A) (H : s S), s
theorem algebra.mem_Inf {R : Type u} {A : Type v} [semiring A] [ A] {S : set A)} {x : A} :
x ∀ (p : A), p Sx p
@[simp]
theorem algebra.Inf_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] (S : set A)) :
@[simp]
theorem algebra.Inf_to_subsemiring {R : Type u} {A : Type v} [semiring A] [ A] (S : set A)) :
@[simp, norm_cast]
theorem algebra.coe_infi {R : Type u} {A : Type v} [semiring A] [ A] {ι : Sort u_1} {S : ι → A} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
theorem algebra.mem_infi {R : Type u} {A : Type v} [semiring A] [ A] {ι : Sort u_1} {S : ι → A} {x : A} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i
@[simp]
theorem algebra.infi_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] {ι : Sort u_1} (S : ι → A) :
(⨅ (i : ι), S i).to_submodule = ⨅ (i : ι), (S i).to_submodule
@[protected, instance]
def algebra.subalgebra.inhabited {R : Type u} {A : Type v} [semiring A] [ A] :
Equations
theorem algebra.mem_bot {R : Type u} {A : Type v} [semiring A] [ A] {x : A} :
theorem algebra.to_submodule_bot {R : Type u} {A : Type v} [semiring A] [ A] :
@[simp]
theorem algebra.coe_bot {R : Type u} {A : Type v} [semiring A] [ A] :
theorem algebra.eq_top_iff {R : Type u} {A : Type v} [semiring A] [ A] {S : A} :
S = ∀ (x : A), x S
@[simp]
theorem algebra.range_id {R : Type u} {A : Type v} [semiring A] [ A] :
A).range =
@[simp]
theorem algebra.map_top {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) :
@[simp]
theorem algebra.map_bot {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) :
@[simp]
theorem algebra.comap_top {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (f : A →ₐ[R] B) :
def algebra.to_top {R : Type u} {A : Type v} [semiring A] [ A] :

`alg_hom` to `⊤ : subalgebra R A`.

Equations
theorem algebra.surjective_algebra_map_iff {R : Type u} {A : Type v} [semiring A] [ A] :
theorem algebra.bijective_algebra_map_iff {R : Type u_1} {A : Type u_2} [field R] [semiring A] [nontrivial A] [ A] :
noncomputable def algebra.bot_equiv_of_injective {R : Type u} {A : Type v} [semiring A] [ A] (h : function.injective A)) :

The bottom subalgebra is isomorphic to the base ring.

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

The bottom subalgebra is isomorphic to the field.

Equations
@[simp]
theorem algebra.bot_equiv_symm_apply (F : Type u_1) (R : Type u_2) [field F] [semiring R] [nontrivial R] [ R] (ᾰ : F) :
R).symm) = )
@[simp]
theorem subalgebra.top_equiv_symm_apply_coe {R : Type u} {A : Type v} [semiring A] [ A] (ᾰ : A) :
@[simp]
theorem subalgebra.top_equiv_apply {R : Type u} {A : Type v} [semiring A] [ A] (ᾰ : ) :
def subalgebra.top_equiv {R : Type u} {A : Type v} [semiring A] [ A] :

The top subalgebra is isomorphic to the algebra.

This is the algebra version of `submodule.top_equiv`.

Equations
theorem subalgebra.subsingleton_of_subsingleton {R : Type u} {A : Type v} [semiring A] [ A] [subsingleton A] :
theorem alg_hom.subsingleton {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] [subsingleton A)] :

For performance reasons this is not an instance. If you need this instance, add

``````local attribute [instance] alg_hom.subsingleton subalgebra.subsingleton_of_subsingleton
``````

in the section that needs it.

theorem alg_equiv.subsingleton_left {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] [subsingleton A)] :
theorem alg_equiv.subsingleton_right {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] [subsingleton B)] :
theorem subalgebra.range_val {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
S.val.range = S
@[protected, instance]
def subalgebra.unique {R : Type u}  :
Equations
def subalgebra.inclusion {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} (h : S 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
theorem subalgebra.inclusion_injective {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} (h : S T) :
@[simp]
theorem subalgebra.inclusion_self {R : Type u} {A : Type v} [semiring A] [ A] {S : A} :
@[simp]
theorem subalgebra.inclusion_mk {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} (h : S T) (x : A) (hx : x S) :
x, hx⟩ = x, _⟩
theorem subalgebra.inclusion_right {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} (h : S T) (x : T) (m : x S) :
x, m⟩ = x
@[simp]
theorem subalgebra.inclusion_inclusion {R : Type u} {A : Type v} [semiring A] [ A] {S T U : A} (hst : S T) (htu : T U) (x : S) :
@[simp]
theorem subalgebra.coe_inclusion {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} (h : S T) (s : S) :
s) = s
def subalgebra.equiv_of_eq {R : Type u} {A : Type v} [semiring A] [ A] (S T : A) (h : S = 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
@[simp]
theorem subalgebra.equiv_of_eq_apply {R : Type u} {A : Type v} [semiring A] [ A] (S T : A) (h : S = T) (x : S) :
(S.equiv_of_eq T h) x = x, _⟩
@[simp]
theorem subalgebra.equiv_of_eq_symm {R : Type u} {A : Type v} [semiring A] [ A] (S T : A) (h : S = T) :
@[simp]
theorem subalgebra.equiv_of_eq_rfl {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
@[simp]
theorem subalgebra.equiv_of_eq_trans {R : Type u} {A : Type v} [semiring A] [ A] (S T U : 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 _
def subalgebra.prod {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : A) (S₁ : B) :
(A × B)

The product of two subalgebras is a subalgebra.

Equations
@[simp]
theorem subalgebra.coe_prod {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : A) (S₁ : B) :
(S.prod S₁) = S ×ˢ S₁
theorem subalgebra.prod_to_submodule {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : A) (S₁ : B) :
(S.prod S₁).to_submodule =
@[simp]
theorem subalgebra.mem_prod {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S : A} {S₁ : B} {x : A × B} :
x S.prod S₁ x.fst S x.snd S₁
@[simp]
theorem subalgebra.prod_top {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] :
theorem subalgebra.prod_mono {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S T : A} {S₁ T₁ : B} :
S TS₁ T₁S.prod S₁ T.prod T₁
@[simp]
theorem subalgebra.prod_inf_prod {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {S T : A} {S₁ T₁ : B} :
S.prod S₁ T.prod T₁ = (S T).prod (S₁ T₁)
theorem subalgebra.coe_supr_of_directed {R : Type u} {A : Type v} [semiring A] [ A] {ι : Type u_1} [nonempty ι] {S : ι → A} (dir : S) :
(supr S) = ⋃ (i : ι), (S i)
noncomputable def subalgebra.supr_lift {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {ι : Type u_1} [nonempty ι] (K : ι → A) (dir : K) (f : Π (i : ι), (K i) →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp ) (T : A) (hT : T = supr K) :

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
@[simp]
theorem subalgebra.supr_lift_inclusion {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {ι : Type u_1} [nonempty ι] {K : ι → A} {dir : K} {f : Π (i : ι), (K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp } {T : A} {hT : T = supr K} {i : ι} (x : (K i)) (h : K i T) :
dir f hf T hT) x) = (f i) x
@[simp]
theorem subalgebra.supr_lift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {ι : Type u_1} [nonempty ι] {K : ι → A} {dir : K} {f : Π (i : ι), (K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp } {T : A} {hT : T = supr K} {i : ι} (h : K i T) :
dir f hf T hT).comp = f i
@[simp]
theorem subalgebra.supr_lift_mk {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {ι : Type u_1} [nonempty ι] {K : ι → A} {dir : K} {f : Π (i : ι), (K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp } {T : A} {hT : T = supr K} {i : ι} (x : (K i)) (hx : x T) :
dir f hf T hT) x, hx⟩ = (f i) x
theorem subalgebra.supr_lift_of_mem {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] {ι : Type u_1} [nonempty ι] {K : ι → A} {dir : K} {f : Π (i : ι), (K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp } {T : A} {hT : T = supr K} {i : ι} (x : T) (hx : x K i) :
dir f hf T hT) x = (f i) x, hx⟩

## Actions by `subalgebra`s #

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

@[protected, instance]
def subalgebra.has_scalar {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} [ α] (S : A) :
α

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

Equations
theorem subalgebra.smul_def {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} [ α] {S : A} (g : S) (m : α) :
g m = g m
@[protected, instance]
def subalgebra.smul_comm_class_left {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] (S : A) :
β
@[protected, instance]
def subalgebra.smul_comm_class_right {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] (S : A) :
β
@[protected, instance]
def subalgebra.is_scalar_tower_left {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} {β : Type u_2} [ β] [ α] [ β] [ β] (S : A) :
β

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

@[protected, instance]
def subalgebra.has_faithful_smul {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} [ α] [ α] (S : A) :
@[protected, instance]
def subalgebra.mul_action {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} [ α] (S : A) :
α

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

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

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

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

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

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

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

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

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

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

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

Equations
theorem subalgebra.algebra_map_eq {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring α] [ A] [ α] (S : A) :
α = α).comp (S.val)
@[simp]
theorem subalgebra.srange_algebra_map {R : Type u_1} {A : Type u_2} [ A] (S : A) :
@[simp]
theorem subalgebra.range_algebra_map {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (S : A) :
@[protected, instance]
def subalgebra.no_zero_smul_divisors_top {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
theorem set.algebra_map_mem_center {R : Type u} {A : Type v} [semiring A] [ A] (r : R) :
A) r
def subalgebra.center (R : Type u) (A : Type v) [semiring A] [ A] :
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`
theorem subalgebra.coe_center (R : Type u) (A : Type v) [semiring A] [ A] :
A) =
@[simp]
theorem subalgebra.center_to_subsemiring (R : Type u) (A : Type v) [semiring A] [ A] :
@[simp]
theorem subalgebra.center_to_subring (R : Type u_1) (A : Type u_2) [comm_ring R] [ring A] [ A] :
@[simp]
theorem subalgebra.center_eq_top (R : Type u) (A : Type u_1) [ A] :
@[protected, instance]
def subalgebra.center.comm_semiring {R : Type u} {A : Type v} [semiring A] [ A] :
Equations
@[protected, instance]
def subalgebra.center.comm_ring {R : Type u} {A : Type u_1} [ring A] [ A] :
Equations
theorem subalgebra.mem_center_iff {R : Type u} {A : Type v} [semiring A] [ A] {a : A} :
a ∀ (b : A), b * a = a * b
@[simp]
theorem set.algebra_map_mem_centralizer {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} (r : R) :
def subalgebra.centralizer (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) :
A

The centralizer of a set as a subalgebra.

Equations
@[simp, norm_cast]
theorem subalgebra.coe_centralizer (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) :
theorem subalgebra.mem_centralizer_iff (R : Type u) {A : Type v} [semiring A] [ A] {s : set A} {z : A} :
∀ (g : A), g sg * z = z * g
theorem subalgebra.centralizer_le (R : Type u) {A : Type v} [semiring A] [ A] (s t : set A) (h : s t) :
@[simp]
theorem subalgebra.centralizer_univ (R : Type u) {A : Type v} [semiring A] [ A] :
def subalgebra_of_subsemiring {R : Type u_1} [semiring R] (S : subsemiring R) :

A subsemiring is a `ℕ`-subalgebra.

Equations
@[simp]
theorem mem_subalgebra_of_subsemiring {R : Type u_1} [semiring R] {x : R} {S : subsemiring R} :
x S
def subalgebra_of_subring {R : Type u_1} [ring R] (S : subring R) :

A subring is a `ℤ`-subalgebra.

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