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} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) :
Subalgebra.toSubmodule S * Subalgebra.toSubmodule T Subalgebra.toSubmodule (S T)
@[simp]
theorem Subalgebra.mul_self {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
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} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) :
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} [CommSemiring R] [Semiring A] [Algebra R A] {R' : Type u_3} [Semiring R'] [MulSemiringAction R' A] [SMulCommClass 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
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) :
    (m S) = m S
    @[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) :
    (m S).toSubsemiring = m S.toSubsemiring
    @[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) :
    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'] [CommRing R] [Ring A] [MulSemiringAction R' A] [Algebra R A] [SMulCommClass R' R A] (m : R') (S : Subalgebra R A) :
    (m S).toSubring = m S.toSubring
    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) :
    r Sm r m S
    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
    • =