mathlib documentation

algebra.algebra.subalgebra.pointwise

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

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

When A is commutative, subalgebra.mul_to_submodule_le is strict.

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

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

This is available as an instance in the pointwise locale.

Equations
@[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) :
(m S) = m S
@[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) :
@[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) :
@[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) :
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) :
r Sm r m S