Pointwise actions on subalgebras. #
If R' acts on an R-algebra A (so that R' and R actions commute)
then we get an R' action on the collection of R-subalgebras.
theorem
subalgebra.mul_to_submodule_le
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
(S T : subalgebra R A) :
(S.to_submodule) * T.to_submodule ≤ (S ⊔ T).to_submodule
@[simp]
theorem
subalgebra.mul_self
{R : Type u_1}
{A : Type u_2}
[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.
theorem
subalgebra.mul_to_submodule
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(S T : subalgebra R A) :
(S.to_submodule) * T.to_submodule = (S ⊔ T).to_submodule
When A is commutative, subalgebra.mul_to_submodule_le is strict.
@[protected, instance]
def
subalgebra.pointwise_mul_action
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
{R' : Type u_3}
[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 := _}
@[simp]
theorem
subalgebra.coe_pointwise_smul
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
{R' : Type u_3}
[semiring R']
[mul_semiring_action R' A]
[smul_comm_class R' R A]
(m : R')
(S : subalgebra R A) :
@[simp]
theorem
subalgebra.pointwise_smul_to_subsemiring
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
{R' : Type u_3}
[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
@[simp]
theorem
subalgebra.pointwise_smul_to_submodule
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
{R' : Type u_3}
[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
@[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
theorem
subalgebra.smul_mem_pointwise_smul
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
{R' : Type u_3}
[semiring R']
[mul_semiring_action R' A]
[smul_comm_class R' R A]
(m : R')
(r : A)
(S : subalgebra R A) :