mathlib3 documentation

algebra.algebra.subalgebra.pointwise

Pointwise actions on subalgebras. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
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) :
⇑subalgebra.to_submodule S * ⇑subalgebra.to_submodule T ≤ ⇑subalgebra.to_submodule (S ⊔ T)
source
@[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) :
⇑subalgebra.to_submodule S * ⇑subalgebra.to_submodule S = ⇑subalgebra.to_submodule S

As submodules, subalgebras are idempotent.

source
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) :
⇑subalgebra.to_submodule S * ⇑subalgebra.to_submodule T = ⇑subalgebra.to_submodule (S ⊔ T)

When A is commutative, subalgebra.mul_to_submodule_le is strict.

source
@[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] :
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
source
@[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
source
@[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
source
@[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) :
⇑subalgebra.to_submodule (m • S) = m • ⇑subalgebra.to_submodule S
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_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 ∈ S → m • r ∈ m • S