# Documentation

Mathlib.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_toSubmodule_le {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (S : ) (T : ) :
Subalgebra.toSubmodule S * Subalgebra.toSubmodule T Subalgebra.toSubmodule (S T)
@[simp]
theorem Subalgebra.mul_self {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (S : ) :
Subalgebra.toSubmodule S * Subalgebra.toSubmodule S = Subalgebra.toSubmodule S

As submodules, subalgebras are idempotent.

theorem Subalgebra.mul_toSubmodule {R : Type u_3} {A : Type u_4} [] [] [Algebra R A] (S : ) (T : ) :
Subalgebra.toSubmodule S * Subalgebra.toSubmodule T = Subalgebra.toSubmodule (S T)

When A is commutative, Subalgebra.mul_toSubmodule_le is strict.

def Subalgebra.pointwiseMulAction {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {R' : Type u_3} [Semiring R'] [] [SMulCommClass R' R A] :
MulAction R' ()

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

This is available as an instance in the pointwise locale.

Instances For
@[simp]
theorem Subalgebra.coe_pointwise_smul {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {R' : Type u_3} [Semiring R'] [] [SMulCommClass R' R A] (m : R') (S : ) :
↑(m S) = m S
@[simp]
theorem Subalgebra.pointwise_smul_toSubsemiring {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {R' : Type u_3} [Semiring R'] [] [SMulCommClass R' R A] (m : R') (S : ) :
(m S).toSubsemiring = m S.toSubsemiring
@[simp]
theorem Subalgebra.pointwise_smul_toSubmodule {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {R' : Type u_3} [Semiring R'] [] [SMulCommClass R' R A] (m : R') (S : ) :
Subalgebra.toSubmodule (m S) = m Subalgebra.toSubmodule S
@[simp]
theorem Subalgebra.pointwise_smul_toSubring {R' : Type u_4} {R : Type u_5} {A : Type u_6} [Semiring R'] [] [Ring A] [] [Algebra R A] [SMulCommClass R' R A] (m : R') (S : ) :
theorem Subalgebra.smul_mem_pointwise_smul {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {R' : Type u_3} [Semiring R'] [] [SMulCommClass R' R A] (m : R') (r : A) (S : ) :
r Sm r m S