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.

source
theorem Subalgebra.mul_toSubmodule_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) :
Subalgebra.toSubmodule S * Subalgebra.toSubmodule T ≤ Subalgebra.toSubmodule (S ⊔ T)
source
@[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.

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

When A is commutative, Subalgebra.mul_toSubmodule_le is strict.

source
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
Instances For
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    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 ∈ S → m • r ∈ m • S
    source
    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
    • ⋯ = ⋯