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}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
(T : Subalgebra R A)
:
@[simp]
theorem
Subalgebra.mul_self
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
As submodules, subalgebras are idempotent.
theorem
Subalgebra.mul_toSubmodule
{R : Type u_3}
{A : Type u_4}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(S : Subalgebra R A)
(T : Subalgebra R A)
:
When A
is commutative, Subalgebra.mul_toSubmodule_le
is strict.
def
Subalgebra.pointwiseMulAction
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{R' : Type u_3}
[Semiring R']
[MulSemiringAction R' A]
[SMulCommClass R' R A]
:
MulAction 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.pointwiseMulAction = MulAction.mk ⋯ ⋯
Instances For
@[simp]
theorem
Subalgebra.coe_pointwise_smul
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{R' : Type u_3}
[Semiring R']
[MulSemiringAction R' A]
[SMulCommClass R' R A]
(m : R')
(S : Subalgebra R A)
:
@[simp]
theorem
Subalgebra.pointwise_smul_toSubsemiring
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{R' : Type u_3}
[Semiring R']
[MulSemiringAction R' A]
[SMulCommClass R' R A]
(m : R')
(S : Subalgebra R A)
:
@[simp]
theorem
Subalgebra.pointwise_smul_toSubmodule
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{R' : Type u_3}
[Semiring R']
[MulSemiringAction R' A]
[SMulCommClass R' R A]
(m : R')
(S : Subalgebra R A)
:
@[simp]
theorem
Subalgebra.pointwise_smul_toSubring
{R' : Type u_4}
{R : Type u_5}
{A : Type u_6}
[Semiring R']
[CommRing R]
[Ring A]
[MulSemiringAction R' A]
[Algebra R A]
[SMulCommClass R' R A]
(m : R')
(S : Subalgebra R A)
:
theorem
Subalgebra.smul_mem_pointwise_smul
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{R' : Type u_3}
[Semiring R']
[MulSemiringAction R' A]
[SMulCommClass R' R A]
(m : R')
(r : A)
(S : Subalgebra R A)
:
instance
Subalgebra.instCovariantClassHSMulLe
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{R' : Type u_3}
[Semiring R']
[MulSemiringAction R' A]
[SMulCommClass R' R A]
:
CovariantClass R' (Subalgebra R A) HSMul.hSMul LE.le
Equations
- ⋯ = ⋯