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)
[comm_semiring R]
[semiring A]
[algebra R A] :
Type v
- carrier : set A
- mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ 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) :
Reinterpret a subalgebra as a subsemiring.
@[protected, instance]
def
subalgebra.set_like
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
set_like (subalgebra R A) A
Equations
- subalgebra.set_like = {coe := subalgebra.carrier _inst_3, coe_injective' := _}
@[protected, instance]
def
subalgebra.subsemiring_class
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
subsemiring_class (subalgebra R A) A
Equations
- subalgebra.subsemiring_class = {to_submonoid_class := {to_mul_mem_class := {mul_mem := _}, one_mem := _}, add_mem := _, zero_mem := _}
@[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} :
@[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
@[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
@[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
theorem
subalgebra.to_subsemiring_injective
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
theorem
subalgebra.to_subsemiring_inj
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S U : subalgebra R A} :
S.to_subsemiring = U.to_subsemiring ↔ S = U
@[protected]
def
subalgebra.copy
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
(s : set A)
(hs : s = ↑S) :
subalgebra R A
Copy of a subalgebra with a new carrier equal to the old one. Useful to fix definitional
equalities.
@[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) :
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) :
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
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
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
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
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) :
@[protected]
theorem
subalgebra.one_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
1 ∈ S
@[protected]
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) :
@[protected]
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 : ℕ) :
@[protected]
theorem
subalgebra.zero_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
0 ∈ S
@[protected]
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) :
@[protected]
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 : ℕ) :
@[protected]
theorem
subalgebra.coe_nat_mem
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
(n : ℕ) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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
@[protected]
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) :
@[protected]
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
@[protected, instance]
def
subalgebra.subring_class
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A] :
subring_class (subalgebra R A) A
Equations
@[protected]
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) :
@[protected]
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) :
@[protected]
theorem
subalgebra.zsmul_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 : ℤ) :
@[protected]
theorem
subalgebra.coe_int_mem
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A)
(n : ℤ) :
def
subalgebra.to_add_submonoid
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R 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}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R 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]
[algebra R A]
(S : subalgebra R A) :
subring A
A subalgebra over a ring is also a subring.
@[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
@[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
theorem
subalgebra.to_subring_injective
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A] :
theorem
subalgebra.to_subring_inj
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
{S U : subalgebra R A} :
S.to_subring = U.to_subring ↔ S = U
@[protected, instance]
def
subalgebra.inhabited
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
subalgebras inherit structure from their subsemiring / semiring coercions.
@[protected, instance]
def
subalgebra.to_semiring
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_comm_semiring
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_ring
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
- S.to_ring = S.to_subring.to_ring
@[protected, instance]
def
subalgebra.to_comm_ring
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_ordered_semiring
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[ordered_semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_ordered_comm_semiring
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[ordered_comm_semiring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_ordered_ring
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ordered_ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_ordered_comm_ring
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ordered_comm_ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_linear_ordered_semiring
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[linear_ordered_semiring A]
[algebra R A]
(S : subalgebra R A) :
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]
[linear_ordered_ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
@[protected, instance]
def
subalgebra.to_linear_ordered_comm_ring
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[linear_ordered_comm_ring A]
[algebra R A]
(S : subalgebra R A) :
Equations
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
@[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
@[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
theorem
subalgebra.to_submodule_injective
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
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
subalgebras inherit structure from their submodule coercions.
@[protected, 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] :
Equations
- S.module' = S.to_submodule.module'
@[protected, instance]
def
subalgebra.module
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
@[protected, 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
@[protected, 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] :
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' := _}
@[protected, instance]
def
subalgebra.algebra
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
@[protected, instance]
def
subalgebra.no_zero_smul_divisors_bot
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
[no_zero_smul_divisors R A] :
@[protected]
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) :
@[protected]
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) :
@[protected]
theorem
subalgebra.coe_zero
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
@[protected]
theorem
subalgebra.coe_one
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
@[simp, norm_cast]
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) :
@[simp, norm_cast]
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
@[protected]
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 : ℕ) :
@[protected]
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} :
@[protected]
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} :
def
subalgebra.val
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
Embedding of a subalgebra into the algebra.
@[simp]
theorem
subalgebra.coe_val
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
theorem
subalgebra.val_apply
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A)
(x : ↥S) :
@[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)
@[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)
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
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, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
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} :
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₂
@[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
theorem
subalgebra.map_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}
{f : A →ₐ[R] B} :
(S.map f).to_submodule = submodule.map f.to_linear_map S.to_submodule
theorem
subalgebra.map_to_subsemiring
{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} :
(S.map f).to_subsemiring = subsemiring.map f.to_ring_hom S.to_subsemiring
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, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
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} :
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)
@[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) :
@[protected, instance]
def
subalgebra.no_zero_divisors
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[no_zero_divisors A]
[algebra R A]
(S : subalgebra R A) :
@[protected, 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) :
def
submodule.to_subalgebra
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
(p : submodule R A)
(h_one : 1 ∈ p)
(h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) :
subalgebra R A
A submodule containing 1 and closed under multiplication is a subalgebra.
Equations
- p.to_subalgebra h_one h_mul = {carrier := p.carrier, mul_mem' := h_mul, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
@[simp]
theorem
submodule.mem_to_subalgebra
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
{p : submodule R A}
{h_one : 1 ∈ p}
{h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * 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}
[comm_semiring R]
[semiring A]
[algebra R A]
(p : submodule R A)
(h_one : 1 ∈ p)
(h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) :
↑(p.to_subalgebra h_one h_mul) = ↑p
@[simp]
theorem
submodule.to_subalgebra_mk
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A)
(h0 : 0 ∈ s)
(hadd : ∀ {a b : A}, a ∈ s → b ∈ s → a + b ∈ s)
(hsmul : ∀ (c : R) {x : A}, x ∈ s → c • 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}) :
@[simp]
theorem
submodule.to_subalgebra_to_submodule
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
(p : submodule R A)
(h_one : 1 ∈ p)
(h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * 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}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
S.to_submodule.to_subalgebra _ _ = S
@[protected]
def
alg_hom.range
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
[semiring B]
[algebra R B]
(φ : A →ₐ[R] B) :
subalgebra R B
Range of an alg_hom as a subalgebra.
def
alg_hom.cod_restrict
{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)
(S : subalgebra R B)
(hf : ∀ (x : A), ⇑f x ∈ 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' := _}
@[simp]
theorem
alg_hom.val_comp_cod_restrict
{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)
(S : subalgebra R 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}
[comm_semiring R]
[semiring A]
[algebra R A]
[semiring B]
[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
theorem
alg_hom.injective_cod_restrict
{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)
(S : subalgebra R B)
(hf : ∀ (x : A), ⇑f x ∈ S) :
function.injective ⇑(f.cod_restrict S hf) ↔ function.injective ⇑f
def
alg_hom.range_restrict
{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) :
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 _
def
alg_hom.equalizer
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
[semiring B]
[algebra R B]
(ϕ ψ : A →ₐ[R] B) :
subalgebra R A
The equalizer of two R-algebra homomorphisms
@[protected, instance]
def
alg_hom.fintype_range
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[algebra R A]
[semiring B]
[algebra R 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}
[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) :
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.
@[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
@[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
noncomputable
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) :
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}
[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
noncomputable
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) :
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}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(e : A ≃ₐ[R] B)
(S : subalgebra R A)
(ᾰ : ↥(subsemiring.map e.to_ring_equiv.to_ring_hom S.to_subsemiring)) :
⇑((e.subalgebra_map S).symm) ᾰ = (e.to_ring_equiv.subsemiring_map S.to_subsemiring).inv_fun ᾰ
@[simp]
theorem
alg_equiv.subalgebra_map_apply
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(e : A ≃ₐ[R] B)
(S : subalgebra R A)
(ᾰ : ↥(S.to_subsemiring)) :
⇑(e.subalgebra_map S) ᾰ = (e.to_ring_equiv.subsemiring_map S.to_subsemiring).to_fun ᾰ
def
alg_equiv.subalgebra_map
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(e : A ≃ₐ[R] B)
(S : subalgebra R 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
- e.subalgebra_map S = {to_fun := (e.to_ring_equiv.subsemiring_map S.to_subsemiring).to_fun, inv_fun := (e.to_ring_equiv.subsemiring_map S.to_subsemiring).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
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, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
@[protected]
@[protected]
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 := _}
@[protected, instance]
def
algebra.subalgebra.complete_lattice
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
complete_lattice (subalgebra R A)
@[simp]
@[simp]
theorem
algebra.mem_top
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{x : A} :
@[simp]
theorem
algebra.top_to_submodule
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
@[simp]
theorem
algebra.top_to_subsemiring
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
@[simp]
@[simp]
theorem
algebra.to_submodule_eq_top
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S : subalgebra R A} :
@[simp]
theorem
algebra.to_subsemiring_eq_top
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S : subalgebra R A} :
@[simp]
theorem
algebra.to_subring_eq_top
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{S : subalgebra R A} :
theorem
algebra.mem_sup_left
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S T : subalgebra R A}
{x : A} :
theorem
algebra.mem_sup_right
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S T : subalgebra R A}
{x : A} :
theorem
algebra.mul_mem_sup
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S T : subalgebra R A}
{x y : A}
(hx : x ∈ S)
(hy : y ∈ T) :
@[simp, norm_cast]
theorem
algebra.coe_inf
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S T : subalgebra R A) :
@[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} :
@[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
@[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
@[simp, norm_cast]
theorem
algebra.coe_Inf
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : set (subalgebra R A)) :
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} :
@[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)
@[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)
@[simp, norm_cast]
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} :
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} :
@[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
@[protected, instance]
def
algebra.subalgebra.inhabited
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
inhabited (subalgebra R A)
Equations
theorem
algebra.mem_bot
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{x : A} :
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}
@[simp]
theorem
algebra.eq_top_iff
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S : subalgebra R A} :
@[simp]
theorem
algebra.range_id
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
(alg_hom.id R A).range = ⊤
alg_hom to ⊤ : subalgebra R A.
Equations
- algebra.to_top = (alg_hom.id R A).cod_restrict ⊤ algebra.to_top._proof_1
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) ↔ ⊤ = ⊥
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) ↔ ⊤ = ⊥
noncomputable
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)) :
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]
[algebra F 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]
[algebra F R]
(ᾰ : F) :
⇑((algebra.bot_equiv F R).symm) ᾰ = ⇑(algebra.of_id F ↥⊥) ᾰ
@[simp]
theorem
subalgebra.top_equiv_symm_apply_coe
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(ᾰ : A) :
↑(⇑(subalgebra.top_equiv.symm) ᾰ) = ᾰ
@[simp]
theorem
subalgebra.top_equiv_apply
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(ᾰ : ↥⊤) :
The top subalgebra is isomorphic to the algebra.
This is the algebra version of submodule.top_equiv.
Equations
- subalgebra.top_equiv = alg_equiv.of_alg_hom ⊤.val algebra.to_top subalgebra.top_equiv._proof_1 subalgebra.top_equiv._proof_2
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)
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.
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)
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)
theorem
subalgebra.range_val
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
@[protected, instance]
Equations
- subalgebra.unique = {to_inhabited := {default := default algebra.subalgebra.inhabited}, uniq := _}
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) :
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' := _}
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) :
@[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
@[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
@[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
@[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
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) :
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.
@[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, _⟩
@[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 _
@[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) :
@[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 _
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.
@[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) :
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
@[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} :
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} :
@[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} :
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) :
noncomputable
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) :
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.
@[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
@[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
@[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) :
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) :
Actions by subalgebras #
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}
[comm_semiring R]
[semiring A]
[algebra R A]
{α : Type u_1}
[has_scalar A α]
(S : subalgebra R A) :
has_scalar ↥S α
The action by a subalgebra is the action by the underlying algebra.
Equations
theorem
subalgebra.smul_def
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{α : Type u_1}
[has_scalar A α]
{S : subalgebra R A}
(g : ↥S)
(m : α) :
@[protected, 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}
[has_scalar A β]
[has_scalar α β]
[smul_comm_class A α β]
(S : subalgebra R A) :
smul_comm_class ↥S α β
@[protected, 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 α β]
[has_scalar A β]
[smul_comm_class α A β]
(S : subalgebra R A) :
smul_comm_class α ↥S β
@[protected, 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 α β]
[has_scalar A α]
[has_scalar 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.
@[protected, instance]
def
subalgebra.has_faithful_scalar
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{α : Type u_1}
[has_scalar A α]
[has_faithful_scalar A α]
(S : subalgebra R A) :
@[protected, 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 algebra.
Equations
@[protected, 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) :
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}
[comm_semiring R]
[semiring A]
[algebra R A]
{α : Type u_1}
[has_zero α]
[smul_with_zero A α]
(S : subalgebra R A) :
smul_with_zero ↥S α
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}
[comm_semiring R]
[semiring A]
[algebra R A]
{α : Type u_1}
[has_zero α]
[mul_action_with_zero A α]
(S : subalgebra R 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}
[comm_semiring R]
[semiring A]
[algebra R A]
{α : Type u_1}
[add_comm_monoid α]
[module A α]
(S : subalgebra R 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}
[comm_semiring R]
[comm_semiring A]
[semiring α]
[algebra R A]
[algebra A α]
(S : subalgebra R 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}
[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)
@[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
@[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
@[protected, 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) :
theorem
set.algebra_map_mem_center
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
⇑(algebra_map R A) r ∈ set.center A
def
subalgebra.center
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
subalgebra R A
The center of an algebra is the set of elements which commute with every element. They form a subalgebra.
Equations
- subalgebra.center R A = {carrier := (subsemiring.center A).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
theorem
subalgebra.coe_center
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
↑(subalgebra.center R A) = set.center A
@[simp]
theorem
subalgebra.center_to_subsemiring
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
@[simp]
theorem
subalgebra.center_to_subring
(R : Type u_1)
(A : Type u_2)
[comm_ring R]
[ring A]
[algebra R A] :
(subalgebra.center R A).to_subring = subring.center A
@[simp]
theorem
subalgebra.center_eq_top
(R : Type u)
[comm_semiring R]
(A : Type u_1)
[comm_semiring A]
[algebra R A] :
subalgebra.center R A = ⊤
@[protected, instance]
def
subalgebra.center.comm_semiring
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
@[protected, instance]
def
subalgebra.center.comm_ring
{R : Type u}
[comm_semiring R]
{A : Type u_1}
[ring A]
[algebra R A] :
comm_ring ↥(subalgebra.center R A)
theorem
subalgebra.mem_center_iff
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{a : A} :
@[simp]
theorem
set.algebra_map_mem_centralizer
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
(r : R) :
⇑(algebra_map R A) r ∈ s.centralizer
def
subalgebra.centralizer
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A) :
subalgebra R A
The centralizer of a set as a subalgebra.
Equations
- subalgebra.centralizer R s = {carrier := (subsemiring.centralizer s).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
@[simp, norm_cast]
theorem
subalgebra.coe_centralizer
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A) :
↑(subalgebra.centralizer R s) = s.centralizer
theorem
subalgebra.mem_centralizer_iff
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
{z : A} :
theorem
subalgebra.centralizer_le
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s t : set A)
(h : s ⊆ t) :
@[simp]
theorem
subalgebra.centralizer_univ
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
A subsemiring is a ℕ-subalgebra.
Equations
- subalgebra_of_subsemiring S = {carrier := S.carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
@[simp]
theorem
mem_subalgebra_of_subsemiring
{R : Type u_1}
[semiring R]
{x : R}
{S : subsemiring R} :
x ∈ subalgebra_of_subsemiring S ↔ x ∈ S
A subring is a ℤ-subalgebra.
Equations
- subalgebra_of_subring S = {carrier := S.carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
@[simp]
theorem
mem_subalgebra_of_subring
{R : Type u_1}
[ring R]
{x : R}
{S : subring R} :
x ∈ subalgebra_of_subring S ↔ x ∈ S