# mathlibdocumentation

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.

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.

def subalgebra.to_subsemiring {R : Type u} {A : Type v} [semiring A] [ A] (s : A) :

Reinterpret a subalgebra as a subsemiring.

@[instance]
def subalgebra.subsemiring.has_coe {R : Type u} {A : Type v} [semiring A] [ A] :

Equations
@[instance]
def subalgebra.has_mem {R : Type u} {A : Type v} [semiring A] [ A] :
A)

Equations
theorem subalgebra.mem_coe {R : Type u} {A : Type v} [semiring A] [ A] {x : A} {s : A} :
x s 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

theorem subalgebra.ext_iff {R : Type u} {A : Type v} [semiring A] [ A] {S T : A} :
S = T ∀ (x : A), x S x T

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.one_mem {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
1 S

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

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

theorem subalgebra.pow_mem {R : Type u} {A : Type v} [semiring A] [ A] (S : A) {x : A} (hx : x S) (n : ) :
x ^ n S

theorem subalgebra.zero_mem {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
0 S

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

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

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

theorem subalgebra.nsmul_mem {R : Type u} {A : Type v} [semiring A] [ A] (S : A) {x : A} (hx : x S) (n : ) :
n •ℕ x S

theorem subalgebra.gsmul_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) {x : A} (hx : x S) (n : ) :
n •ℤ x S

theorem subalgebra.coe_nat_mem {R : Type u} {A : Type v} [semiring A] [ A] (S : A) (n : ) :
n S

theorem subalgebra.coe_int_mem {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) (n : ) :
n S

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

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

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

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

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) :
∏ (x : ι) in t, f x S

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) :
∑ (x : ι) in t, f x S

@[instance]
def subalgebra.is_add_submonoid {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :

@[instance]
def subalgebra.is_submonoid {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :

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
@[instance]
def subalgebra.is_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) :

@[instance]
def subalgebra.inhabited {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :

Equations
@[instance]
def subalgebra.semiring (R : Type u) (A : Type v) [semiring A] [ A] (S : A) :

Equations
@[instance]
def subalgebra.comm_semiring (R : Type u) (A : Type v) [ A] (S : A) :

Equations
@[instance]
def subalgebra.ring (R : Type u) (A : Type v) [comm_ring R] [ring A] [ A] (S : A) :

Equations
@[instance]
def subalgebra.comm_ring (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [ A] (S : A) :

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

Equations
@[instance]
def subalgebra.to_algebra {R : Type u_1} {A : Type u_2} {B : Type u_3} [semiring B] [ A] [ B] (A₀ : A) :
algebra A₀ B

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

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

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

Convert a subalgebra to submodule

Equations
@[instance]
def subalgebra.coe_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] :
has_coe A) A)

Equations
@[instance]
def subalgebra.to_submodule.is_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) :

@[simp]
theorem subalgebra.mem_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] (S : A) {x : A} :
x S x S

theorem subalgebra.to_submodule_injective {R : Type u} {A : Type v} [semiring A] [ A] {S U : A} (h : S = U) :
S = U

theorem subalgebra.to_submodule_inj {R : Type u} {A : Type v} [semiring A] [ A] {S U : A} :
S = U S = U

@[simp]
theorem subalgebra.mul_self {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
(S) * S = S

As submodules, subalgebras are idempotent.

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
@[instance]
def subalgebra.partial_order {R : Type u} {A : Type v} [semiring A] [ A] :

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

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

Equations
def subalgebra.under {R : Type u} {A : Type v} {i : A} (S : A) (T : A) :
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
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
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_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_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.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₂

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

@[instance]
def subalgebra.integral_domain {R : Type u_1} {A : Type u_2} [comm_ring R] [ A] (S : A) :

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

Range of an alg_hom as a subalgebra.

Equations
@[simp]
theorem alg_hom.mem_range {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (φ : A →ₐ[R] B) {y : B} :
y φ.range ∃ (x : A), φ x = y

@[simp]
theorem alg_hom.coe_range {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (φ : A →ₐ[R] B) :
(φ.range) =

def alg_hom.cod_restrict {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) (S : B) (hf : ∀ (x : A), f x S) :

Restrict the codomain of an algebra homomorphism.

Equations
theorem alg_hom.injective_cod_restrict {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) (S : B) (hf : ∀ (x : A), f x S) :

def alg_hom.equalizer {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ 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] [semiring B] [ A] [ B] (ϕ ψ : A →ₐ[R] B) (x : A) :
x ϕ.equalizer ψ ϕ x = ψ x

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

The minimal subalgebra that includes s.

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

def algebra.gi {R : Type u} {A : Type v} [semiring A] [ A] :

Galois insertion between adjoin and coe.

Equations
@[instance]
def algebra.subalgebra.complete_lattice {R : Type u} {A : Type v} [semiring A] [ A] :

Equations
@[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] :
= {1}

@[simp]
theorem algebra.mem_top {R : Type u} {A : Type v} [semiring A] [ A] {x : A} :

@[simp]
theorem algebra.coe_top {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.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] :

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

The top subalgebra is isomorphic to the field.

Equations
theorem subalgebra.range_val {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
S.val.range = S

@[instance]
def subalgebra.unique {R : Type u}  :

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

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

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

@[simp]
theorem mem_subalgebra_of_is_subring {R : Type u_1} [ring R] {x : R} {S : set R} [is_subring S] :
x S