mathlib docs: algebra.algebra.subalgebra

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

Type v

carrier : set A
one_mem' : 1 ∈ c.carrier
mul_mem' : ∀ {a b : A}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
zero_mem' : 0 ∈ c.carrier
add_mem' : ∀ {a b : A}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ c.carrier

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

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

subsemiring A

Reinterpret a subalgebra as a subsemiring.

source

@[instance]

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

has_coe (subalgebra R A) (subsemiring A)

Equations

subalgebra.subsemiring.has_coe = {coe := λ (S : subalgebra R A), {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _}}

source

@[instance]

def subalgebra.has_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

has_mem A (subalgebra R A)

Equations

subalgebra.has_mem = {mem := λ (x : A) (S : subalgebra R A), x ∈ ↑S}

source

theorem subalgebra.mem_coe {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {x : A} {s : subalgebra R A} :

x ∈ ↑s ↔ 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

theorem subalgebra.ext_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} :

S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T

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

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

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

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

S.to_subring = {carrier := S.to_subsemiring.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, neg_mem' := _}

source

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

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

S.inhabited = {default := 0}

source

@[instance]

def subalgebra.semiring (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

semiring ↥S

Equations

subalgebra.semiring R A S = ↑S.to_semiring

source

@[instance]

def subalgebra.comm_semiring (R : Type u) (A : Type v) [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) :

comm_semiring ↥S

Equations

subalgebra.comm_semiring R A S = ↑S.to_comm_semiring

source

@[instance]

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

ring ↥S

Equations

subalgebra.ring R A S = subtype.ring

source

@[instance]

def subalgebra.comm_ring (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) :

comm_ring ↥S

Equations

subalgebra.comm_ring R A S = subtype.comm_ring

source

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

S.algebra = {to_has_scalar := {smul := λ (c : R) (x : ↥S), ⟨c • x.val, _⟩}, to_ring_hom := {to_fun := ((algebra_map R A).cod_srestrict ↑S _).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

source

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

A₀.to_algebra = algebra.of_subsemiring ↑A₀

source

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

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

S.val = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

S.to_submodule = {carrier := ↑S, zero_mem' := _, add_mem' := _, smul_mem' := _}

source

@[instance]

def subalgebra.coe_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

has_coe (subalgebra R A) (submodule R A)

Equations

subalgebra.coe_to_submodule = {coe := subalgebra.to_submodule _inst_3}

source

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

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 ↔ x ∈ S

source

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

S = U

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 = ↑U ↔ 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) * ↑S = ↑S

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 ≃ₗ[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

S.to_submodule_equiv = linear_equiv.of_eq ↑S (has_coe_t_aux.coe S) _

source

@[instance]

def subalgebra.partial_order {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

partial_order (subalgebra R A)

Equations

subalgebra.partial_order = {le := λ (S T : subalgebra R A), ↑S ⊆ ↑T, lt := preorder.lt._default (λ (S T : subalgebra R A), ↑S ⊆ ↑T), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

iSB.comap = {carrier := iSB.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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

S.under T = {carrier := T.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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

S.map f = {carrier := (subsemiring.map ↑f ↑S).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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

S.comap' f = {carrier := (subsemiring.comap ↑f ↑S).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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_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

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

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

S.integral_domain = subring.domain ↑S

source

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

φ.range = {carrier := φ.to_ring_hom.srange.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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

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

f.cod_restrict S hf = {to_fun := (↑f.cod_srestrict ↑S hf).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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.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

ϕ.equalizer ψ = {carrier := {a : A | ⇑ϕ a = ⇑ψ a}, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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

algebra.adjoin R s = {carrier := (subsemiring.closure (set.range ⇑(algebra_map R A) ∪ s)).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

source

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

galois_connection (algebra.adjoin R) coe

source

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

algebra.gi = {choice := λ (s : set A) (hs : ↑(algebra.adjoin R s) ≤ s), algebra.adjoin R s, gc := _, le_l_u := _, choice_eq := _}

source

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

algebra.subalgebra.complete_lattice = algebra.gi.lift_complete_lattice

source

@[instance]

def algebra.subalgebra.inhabited {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

inhabited (subalgebra R A)

Equations

algebra.subalgebra.inhabited = {default := ⊥}

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

↑⊥ = 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.coe_top {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :

↑⊤ = ⊤

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

algebra.to_top = {to_fun := λ (x : A), ⟨x, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

algebra.bot_equiv_of_injective h = (alg_equiv.of_bijective (algebra.of_id R ↥⊥) _).symm

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

algebra.bot_equiv F R = algebra.bot_equiv_of_injective _

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

algebra.top_equiv = (alg_equiv.of_bijective algebra.to_top algebra.top_equiv._proof_1).symm

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

@[instance]

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

unique (subalgebra R R)

Equations

subalgebra.unique = {to_inhabited := {default := default (subalgebra R R) algebra.subalgebra.inhabited}, uniq := _}

source

def subalgebra_of_subsemiring {R : Type u_1} [semiring R] (S : subsemiring R) :

subalgebra ℕ R

A subsemiring is a ℕ-subalgebra.

Equations

subalgebra_of_subsemiring S = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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

subalgebra_of_subring S = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

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

subalgebra_of_is_subring S = subalgebra_of_subring S.to_subring

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

mathlib documentation

Subalgebras over Commutative Semiring