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 ∈ self.carrier
mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
zero_mem' : 0 ∈ self.carrier
add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
algebra_map_mem' : ∀ (r : R), ⇑(algebra_map R A) r ∈ self.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] (self : subalgebra R A) :

subsemiring A

Reinterpret a subalgebra as a subsemiring.

source

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

subalgebra.set_like = {coe := subalgebra.carrier _inst_3, coe_injective' := _}

source

@[simp]

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

x ∈ s.carrier ↔ x ∈ s

source

@[ext]

theorem subalgebra.ext {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) :

S = T

source

@[simp]

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

x ∈ S.to_subsemiring ↔ x ∈ S

source

@[simp]

theorem subalgebra.coe_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

↑(S.to_subsemiring) = ↑S

source

def subalgebra.copy {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (s : set A) (hs : s = ↑S) :

subalgebra R A

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

Equations

S.copy s hs = {carrier := s, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

source

@[simp]

theorem subalgebra.coe_copy {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (s : set A) (hs : s = ↑S) :

↑(S.copy s hs) = s

source

theorem subalgebra.copy_eq {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (s : set A) (hs : s = ↑S) :

S.copy s hs = S

source

theorem subalgebra.algebra_map_mem {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) (r : R) :

⇑(algebra_map R A) r ∈ S

source

theorem subalgebra.srange_le {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

(algebra_map R A).srange ≤ S.to_subsemiring

source

theorem subalgebra.range_subset {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

set.range ⇑(algebra_map R A) ⊆ ↑S

source

theorem subalgebra.range_le {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

set.range ⇑(algebra_map R A) ≤ ↑S

source

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

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

add_submonoid A

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

Equations

S.to_add_submonoid = S.to_subsemiring.to_add_submonoid

source

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

submonoid A

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

Equations

S.to_submonoid = S.to_subsemiring.to_submonoid

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

@[simp]

theorem subalgebra.mem_to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {S : subalgebra R A} {x : A} :

x ∈ S.to_subring ↔ x ∈ S

source

@[simp]

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

↑(S.to_subring) = ↑S

source

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

S.to_semiring = S.to_subsemiring.to_semiring

source

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

S.to_comm_semiring = S.to_subsemiring.to_comm_semiring

source

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

S.to_ring = S.to_subring.to_ring

source

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

S.to_comm_ring = S.to_subring.to_comm_ring

source

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

S.to_ordered_semiring = S.to_subsemiring.to_ordered_semiring

source

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

S.to_ordered_comm_semiring = S.to_subsemiring.to_ordered_comm_semiring

source

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

S.to_ordered_ring = S.to_subring.to_ordered_ring

source

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

S.to_ordered_comm_ring = S.to_subring.to_ordered_comm_ring

source

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

S.to_linear_ordered_semiring = S.to_subsemiring.to_linear_ordered_semiring

source

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

S.to_linear_ordered_ring = S.to_subring.to_linear_ordered_ring

source

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

S.to_linear_ordered_comm_ring = S.to_subring.to_linear_ordered_comm_ring

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

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

@[simp]

theorem subalgebra.coe_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

↑(S.to_submodule) = ↑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

@[instance]

def subalgebra.module' {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [semiring R'] [has_scalar R' R] [module R' A] [is_scalar_tower R' R A] :

module R' ↥S

Equations

S.module' = S.to_submodule.module'

source

@[instance]

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

module R ↥S

Equations

S.module = S.module'

source

@[instance]

def subalgebra.is_scalar_tower {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [semiring R'] [has_scalar R' R] [module R' A] [is_scalar_tower R' R A] :

is_scalar_tower R' R ↥S

source

@[instance]

def subalgebra.algebra' {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [comm_semiring R'] [has_scalar R' R] [algebra R' A] [is_scalar_tower R' R A] :

algebra R' ↥S

Equations

S.algebra' = {to_has_scalar := smul_with_zero.to_has_scalar (mul_action_with_zero.to_smul_with_zero R' ↥S), to_ring_hom := {to_fun := ((algebra_map R' A).cod_srestrict S.to_subsemiring _).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

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 = S.algebra'

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

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

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]

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]

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]

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]

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]

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]

theorem subalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [semiring R'] [has_scalar R' R] [module R' A] [is_scalar_tower R' R A] (r : R') (x : ↥S) :

↑(r • x) = r • ↑x

source

@[simp]

theorem subalgebra.coe_algebra_map {R' : Type u'} {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) [comm_semiring R'] [has_scalar R' R] [algebra R' A] [is_scalar_tower R' R A] (r : R') :

↑(⇑(algebra_map R' ↥S) r) = ⇑(algebra_map R' A) r

source

@[simp]

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]

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]

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

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

@[simp]

theorem subalgebra.to_subsemiring_subtype {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

S.to_subsemiring.subtype = ↑(S.val)

source

@[simp]

theorem subalgebra.to_subring_subtype {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :

S.to_subring.subtype = ↑(S.val)

source

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

S.to_submodule_equiv = linear_equiv.of_eq S.to_submodule S.to_submodule _

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.to_subsemiring).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_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

@[simp]

theorem subalgebra.map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

S.map (alg_hom.id R A) = S

source

theorem subalgebra.map_map {R : Type u} {A : Type v} {B C : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (S : subalgebra R A) (g : B →ₐ[R] C) (f : A →ₐ[R] B) :

(S.map f).map g = S.map (g.comp f)

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

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

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.gc_map_comap {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (f : A →ₐ[R] B) :

galois_connection (λ (S : subalgebra R A), S.map f) (λ (S : subalgebra R B), S.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]

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

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

@[instance]

def subalgebra.is_domain {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [is_domain A] [algebra R A] (S : subalgebra R A) :

is_domain ↥S

source

def 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

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

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

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

f.range_restrict = f.cod_restrict f.range _

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

@[instance]

def alg_hom.fintype_range {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [fintype A] [decidable_eq B] (φ : A →ₐ[R] B) :

fintype ↥(φ.range)

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

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

Equations

φ.fintype_range = set.fintype_range ⇑φ

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

alg_equiv.of_left_inverse h = {to_fun := ⇑(f.range_restrict), inv_fun := g ∘ ⇑(f.range.val), left_inv := h, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

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

alg_equiv.of_injective f hf = alg_equiv.of_left_inverse _

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

alg_equiv.of_injective_field f = alg_equiv.of_injective f _

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

@[simp]

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

↑⊤ = set.univ

source

@[simp]

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

x ∈ ⊤

source

@[simp]

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

⊤.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_inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) :

↑(S ⊓ T) = ↑S ∩ ↑T

source

@[simp]

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

x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

source

@[simp]

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

(S ⊓ T).to_submodule = S.to_submodule ⊓ T.to_submodule

source

@[simp]

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

(S ⊓ T).to_subsemiring = S.to_subsemiring ⊓ T.to_subsemiring

source

@[simp]

theorem algebra.coe_Inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : set (subalgebra R A)) :

↑(Inf S) = ⋂ (s : subalgebra R A) (H : s ∈ S), ↑s

source

theorem algebra.mem_Inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : set (subalgebra R A)} {x : A} :

x ∈ Inf S ↔ ∀ (p : subalgebra R A), p ∈ S → x ∈ p

source

@[simp]

theorem algebra.Inf_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : set (subalgebra R A)) :

(Inf S).to_submodule = Inf (subalgebra.to_submodule '' S)

source

@[simp]

theorem algebra.Inf_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : set (subalgebra R A)) :

(Inf S).to_subsemiring = Inf (subalgebra.to_subsemiring '' S)

source

@[simp]

theorem algebra.coe_infi {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Sort u_1} {S : ι → subalgebra R A} :

(↑⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

source

theorem algebra.mem_infi {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Sort u_1} {S : ι → subalgebra R A} {x : A} :

(x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i

source

@[simp]

theorem algebra.infi_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Sort u_1} (S : ι → subalgebra R A) :

(⨅ (i : ι), S i).to_submodule = ⨅ (i : ι), (S i).to_submodule

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

⊥.to_submodule = submodule.span R {1}

source

@[simp]

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

↑⊥ = set.range ⇑(algebra_map R A)

source

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

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

source

@[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 = (alg_hom.id R A).cod_restrict ⊤ algebra.to_top._proof_1

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

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.

source

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

@[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.inclusion {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) :

↥S →ₐ[R] ↥T

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

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

Equations

subalgebra.inclusion h = {to_fun := set.inclusion h, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

theorem subalgebra.inclusion_injective {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) :

function.injective ⇑(subalgebra.inclusion h)

source

@[simp]

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

subalgebra.inclusion _ = alg_hom.id R ↥S

source

@[simp]

theorem subalgebra.inclusion_right {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S) :

⇑(subalgebra.inclusion h) ⟨↑x, m⟩ = x

source

@[simp]

theorem subalgebra.inclusion_inclusion {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T U : subalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S) :

⇑(subalgebra.inclusion htu) (⇑(subalgebra.inclusion hst) x) = ⇑(subalgebra.inclusion _) x

source

@[simp]

theorem subalgebra.coe_inclusion {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S T : subalgebra R A} (h : S ≤ T) (s : ↥S) :

↑(⇑(subalgebra.inclusion h) s) = ↑s

source

def subalgebra.equiv_of_eq {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) (h : S = T) :

↥S ≃ₐ[R] ↥T

Two subalgebras that are equal are also equivalent as algebras.

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

Equations

S.equiv_of_eq T h = {to_fun := λ (x : ↥S), ⟨↑x, _⟩, inv_fun := λ (x : ↥T), ⟨↑x, _⟩, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem subalgebra.equiv_of_eq_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T : subalgebra R A) (h : S = T) (x : ↥S) :

⇑(S.equiv_of_eq T h) x = ⟨↑x, _⟩

source

@[simp]

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

(S.equiv_of_eq T h).symm = T.equiv_of_eq S _

source

@[simp]

theorem subalgebra.equiv_of_eq_rfl {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :

S.equiv_of_eq S rfl = alg_equiv.refl

source

@[simp]

theorem subalgebra.equiv_of_eq_trans {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S T U : subalgebra R A) (hST : S = T) (hTU : T = U) :

(S.equiv_of_eq T hST).trans (T.equiv_of_eq U hTU) = S.equiv_of_eq U _

source

def subalgebra.prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R A) (S₁ : subalgebra R B) :

subalgebra R (A × B)

The product of two subalgebras is a subalgebra.

Equations

S.prod S₁ = {carrier := ↑S.prod ↑S₁, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}

source

@[simp]

theorem subalgebra.coe_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R A) (S₁ : subalgebra R B) :

↑(S.prod S₁) = ↑S.prod ↑S₁

source

theorem subalgebra.prod_to_submodule {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R A) (S₁ : subalgebra R B) :

(S.prod S₁).to_submodule = S.to_submodule.prod S₁.to_submodule

source

@[simp]

theorem subalgebra.mem_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S : subalgebra R A} {S₁ : subalgebra R B} {x : A × B} :

x ∈ S.prod S₁ ↔ x.fst ∈ S ∧ x.snd ∈ S₁

source

@[simp]

theorem subalgebra.prod_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :

⊤.prod ⊤ = ⊤

source

theorem subalgebra.prod_mono {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S T : subalgebra R A} {S₁ T₁ : subalgebra R B} :

S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁

source

@[simp]

theorem subalgebra.prod_inf_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {S T : subalgebra R A} {S₁ T₁ : subalgebra R B} :

S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)

source

theorem subalgebra.coe_supr_of_directed {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {ι : Type u_1} [nonempty ι] {S : ι → subalgebra R A} (dir : directed has_le.le S) :

↑(supr S) = ⋃ (i : ι), ↑(S i)

source

def subalgebra.supr_lift {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] (K : ι → subalgebra R A) (dir : directed has_le.le K) (f : Π (i : ι), ↥(K i) →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)) (T : subalgebra R A) (hT : T = supr K) :

↥T →ₐ[R] B

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

Equations

subalgebra.supr_lift K dir f hf T hT = eq.rec {to_fun := set.Union_lift (λ (i : ι), ↑(K i)) (λ (i : ι) (x : ↥↑(K i)), ⇑(f i) x) _ ↑(supr K) _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _} _

source

@[simp]

theorem subalgebra.supr_lift_inclusion {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] {K : ι → subalgebra R A} {dir : directed has_le.le K} {f : Π (i : ι), ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)} {T : subalgebra R A} {hT : T = supr K} {i : ι} (x : ↥(K i)) (h : K i ≤ T) :

⇑(subalgebra.supr_lift K dir f hf T hT) (⇑(subalgebra.inclusion h) x) = ⇑(f i) x

source

@[simp]

theorem subalgebra.supr_lift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] {ι : Type u_1} [nonempty ι] {K : ι → subalgebra R A} {dir : directed has_le.le K} {f : Π (i : ι), ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (subalgebra.inclusion h)} {T : subalgebra R A} {hT : T = supr K} {i : ι} (h : K i ≤ T) :

(subalgebra.supr_lift K dir f hf T hT).comp (subalgebra.inclusion h) = f i

source

@[simp]

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

⇑(subalgebra.supr_lift K dir f hf T hT) ⟨↑x, hx⟩ = ⇑(f i) x

source

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

⇑(subalgebra.supr_lift K dir f hf T hT) x = ⇑(f i) ⟨↑x, hx⟩

source

@[instance]

def subalgebra.mul_action {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [mul_action A α] (S : subalgebra R A) :

mul_action ↥S α

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

Equations

S.mul_action = S.to_subsemiring.mul_action

source

theorem subalgebra.smul_def {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [mul_action A α] {S : subalgebra R A} (g : ↥S) (m : α) :

g • m = ↑g • m

source

@[instance]

def subalgebra.smul_comm_class_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} {β : Type u_2} [mul_action A β] [has_scalar α β] [smul_comm_class A α β] (S : subalgebra R A) :

smul_comm_class ↥S α β

source

@[instance]

def subalgebra.smul_comm_class_right {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} {β : Type u_2} [has_scalar α β] [mul_action A β] [smul_comm_class α A β] (S : subalgebra R A) :

smul_comm_class α ↥S β

source

@[instance]

def subalgebra.is_scalar_tower_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} {β : Type u_2} [has_scalar α β] [mul_action A α] [mul_action A β] [is_scalar_tower A α β] (S : subalgebra R A) :

is_scalar_tower ↥S α β

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

source

@[instance]

def subalgebra.has_faithful_scalar {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [mul_action A α] [has_faithful_scalar A α] (S : subalgebra R A) :

has_faithful_scalar ↥S α

source

@[instance]

def subalgebra.distrib_mul_action {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [add_monoid α] [distrib_mul_action A α] (S : subalgebra R A) :

distrib_mul_action ↥S α

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

Equations

S.distrib_mul_action = S.to_subsemiring.distrib_mul_action

source

@[instance]

def subalgebra.module_left {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} [add_comm_monoid α] [module A α] (S : subalgebra R A) :

module ↥S α

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

Equations

S.module_left = S.to_subsemiring.module

source

@[instance]

def subalgebra.to_algebra {α : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [semiring α] [algebra R A] [algebra A α] (S : subalgebra R A) :

algebra ↥S α

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

Equations

S.to_algebra = algebra.of_subsemiring S.to_subsemiring

source

theorem subalgebra.algebra_map_eq {α : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [semiring α] [algebra R A] [algebra A α] (S : subalgebra R A) :

algebra_map ↥S α = (algebra_map A α).comp ↑(S.val)

source

@[simp]

theorem subalgebra.srange_algebra_map {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) :

(algebra_map ↥S A).srange = S.to_subsemiring

source

@[simp]

theorem subalgebra.range_algebra_map {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) :

(algebra_map ↥S A).range = S.to_subring

source

@[instance]

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

no_zero_smul_divisors ↥S A

source

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

@[simp]

theorem subalgebra.mem_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} {x : A} :

x ∈ S.under T ↔ x ∈ T

source

@[instance]

def subalgebra.pointwise_mul_action {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {R' : Type u_1} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A] :

mul_action R' (subalgebra R A)

The action on a subalgebra corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations

subalgebra.pointwise_mul_action = {to_has_scalar := {smul := λ (a : R') (S : subalgebra R A), S.map (mul_semiring_action.to_alg_hom R A a)}, one_smul := _, mul_smul := _}

source

@[simp]

theorem subalgebra.coe_pointwise_smul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {R' : Type u_1} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A] (m : R') (S : subalgebra R A) :

↑(m • S) = m • ↑S

source

@[simp]

theorem subalgebra.pointwise_smul_to_subsemiring {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {R' : Type u_1} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A] (m : R') (S : subalgebra R A) :

(m • S).to_subsemiring = m • S.to_subsemiring

source

@[simp]

theorem subalgebra.pointwise_smul_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {R' : Type u_1} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A] (m : R') (S : subalgebra R A) :

(m • S).to_submodule = m • S.to_submodule

source

@[simp]

theorem subalgebra.pointwise_smul_to_subring {R' : Type u_1} {R : Type u_2} {A : Type u_3} [semiring R'] [comm_ring R] [ring A] [mul_semiring_action R' A] [algebra R A] [smul_comm_class R' R A] (m : R') (S : subalgebra R A) :

(m • S).to_subring = m • S.to_subring

source

theorem subalgebra.smul_mem_pointwise_smul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {R' : Type u_1} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A] (m : R') (r : A) (S : subalgebra R A) :

r ∈ S → m • r ∈ m • S

source